# List of theorems

List of theorems in general/First_steps_in_set_theory.gh:

(= B0 B1)(↔ (∈ A B0) (∈ A B1))
(= A0 A1)(↔ (∈ A0 B) (∈ A1 B))
(→ antecedent (= B0 B1))(→ antecedent (↔ (∈ A B0) (∈ A B1)))
(→ antecedent (= A0 A1))(→ antecedent (↔ (∈ A0 B) (∈ A1 B)))
(↔ (∈ A B) (∀ x (→ (= x A) (∈ x B))))
(↔ (∈ A B) (∃ x (∧ (= x A) (∈ x B))))
NotElement Not an element (<code>∉</code>) is just an abbreviation for negation and element-of.
(↔ (∉ A B) (¬ (∈ A B)))
Extensionality-1 Extensionality—various corollaries and convenience theorems (easy consequences of the axiom).
(→ (∀ z (↔ (∈ z A) (∈ z y))) (= A y))
(→ (∀ z (↔ (∈ z A) (∈ z B))) (= A B))
(↔ (∈ x A) (∈ x B))(= A B)
(↔ (= A B) (∀ z (↔ (∈ z A) (∈ z B))))
axnul The first thing we do in terms of constructing sets is the empty set.
(∃ x (∀ y (¬ (∈ y x))))
axnul-with-subst Here is a corollary which we'll use shortly.
(∃ emptySet (∀ y (↔ (∈ y emptySet) (subst y z (⊥)))))
(= (∅) (abstract y (⊥)))
(¬ (∈ x (∅)))
(¬ (∈ A (∅)))
(∃ w (∀ z (↔ (∈ z w) (∨ (= z A) (= z y)))))
(∃ w (∀ z (↔ (∈ z w) (∨ (= z A) (= z B)))))
(→ (= z y) (↔ φz φy)) , (∃ result (∀ y (↔ (∈ y result) φy)))(↔ (∈ y (abstract z φz)) φy)
(→ (= z y) (↔ φz φy)) , (→ (= y C) (↔ φy φC)) , (∃ result (∀ y (↔ (∈ y result) φy)))(↔ (∈ C (abstract z φz)) φC)
(∃ result (∀ element (↔ (∈ element result) (subst element x φx)))) , (∃ result (∀ element (↔ (∈ element result) (subst element y φy)))) , (→ (= x y) (↔ φx φy))(= (abstract x φx) (abstract y φy))
(→ (= C D) (↔ (∨ (= C A) (= C B)) (∨ (= D A) (= D B))))
(↔ (∈ C (abstract z (∨ (= z A) (= z B)))) (∨ (= C A) (= C B)))
(∃ result (∀ element (↔ (∈ element result) (subst element x (∨ (= x A) (= x B))))))
(= (unorderedPair A B) (abstract y (∨ (= y A) (= y B))))
(↔ (∈ C (unorderedPair A B)) (∨ (= C A) (= C B)))
(→ (∧ (= A0 B0) (= A1 B1)) (= (abstract a (∨ (= a A0) (= a A1))) (abstract b (∨ (= b B0) (= b B1)))))
(→ (∧ (= A0 B0) (= A1 B1)) (= (unorderedPair A0 A1) (unorderedPair B0 B1)))
(= (singleton A) (unorderedPair A A))
(↔ (∈ B (singleton A)) (= B A))
(→ (= A B) (= (singleton A) (singleton B)))
(∃ y (∀ z (↔ (∈ z y) (∃ w (∧ (∈ z w) (∈ w A))))))
(→ (= C D) (↔ (∃ x (∧ (∈ C x) (∈ x A))) (∃ x (∧ (∈ D x) (∈ x A)))))
(↔ (∃ x (∧ (∈ C x) (∈ x A))) (∃ x′ (∧ (∈ C x′) (∈ x′ A))))
(↔ (∈ B (abstract z (∃ x′ (∧ (∈ z x′) (∈ x′ A))))) (∃ x (∧ (∈ B x) (∈ x A))))
(∃ result (∀ element (↔ (∈ element result) (subst element z (∃ x (∧ (∈ z x) (∈ x A)))))))
(= (⋃ A) (abstract z (∃ x (∧ (∈ z x) (∈ x A)))))
(↔ (∈ B (⋃ A)) (∃ x (∧ (∈ B x) (∈ x A))))
(↔ (⊆ A B) (∀ x (→ (∈ x A) (∈ x B))))
(→ (∧ (⊆ A B) (⊆ B C)) (⊆ A C))
(↔ (= A B) (∧ (⊆ A B) (⊆ B A)))
(⊆ A A)
(→ (∧ (⊆ A B) (⊆ B A)) (= A B))
(∃ y (∀ z (↔ (∈ z y) (∀ w (→ (∈ w z) (∈ w A))))))
(→ (= C D) (↔ (∀ x (→ (∈ x C) (∈ x A))) (∀ x (→ (∈ x D) (∈ x A)))))
(↔ (∀ x (→ (∈ x C) (∈ x A))) (∀ x′ (→ (∈ x′ C) (∈ x′ A))))
(↔ (∈ B (abstract z (∀ x′ (→ (∈ x′ z) (∈ x′ A))))) (∀ x (→ (∈ x B) (∈ x A))))
(∃ result (∀ element (↔ (∈ element result) (subst element z (∀ x (→ (∈ x z) (∈ x A)))))))
(= (power A) (abstract z (∀ x (→ (∈ x z) (∈ x A)))))
(↔ (∈ B (power A)) (∀ x (→ (∈ x B) (∈ x A))))
(↔ (∈ B (power A)) (⊆ B A))
(∃ y (∀ x (↔ (∈ x y) (∧ (∈ x A) φ))))
(∃ result (∀ y (↔ (∈ y result) (∧ (∈ y A) (subst y x φ)))))
(→ (= C D) (↔ (∧ (∈ C A) (subst C x φ)) (∧ (∈ D A) (subst D x φ))))
(↔ (∈ C (abstract z (∧ (∈ z A) (subst z x φ)))) (∧ (∈ C A) (subst C x φ)))
(∃ result (∀ element (↔ (∈ element result) (subst element z (∧ (∈ z A) (subst z x φ))))))
(= (separate x A φ) (abstract z (∧ (∈ z A) (subst z x φ))))
(↔ (∈ C (separate x A φ)) (∧ (∈ C A) (subst C x φ)))
(↔ (∈ A B) (∀ x (→ (= x A) (∈ x B))))