Created:
V| Parents |
| log |
| Children |
| misc |
| Axioms |
|
bool_cases_axiom
|
⊢ ∀ b• (b ⇔ T) ∨ (b ⇔ F) |
|
⇒_antisym_axiom
|
⊢ ∀ b1 b2• (b1 ⇒ b2) ⇒ (b2 ⇒ b1) ⇒ (b1 ⇔ b2) |
|
η_axiom
|
⊢ ∀ f• (λ x• f x) = f |
|
ε_axiom
|
⊢ ∀ P x• P x ⇒ P ($ε P) |
|
infinity_axiom
|
⊢ ∃ f• OneOne f ∧ ¬ Onto f |