# List of theorems

List of theorems in general/Basic_operations_of_Zermelo-Fraenkel_set_theory.gh:

(∈ A (singleton A))
(∈ A (unorderedPair A B))
(∈ B (unorderedPair A B))
(= (unorderedPair A B) (unorderedPair B A))
(→ (= (unorderedPair A C) (unorderedPair B C)) (∨ (= A B) (= A C)))
(→ (= (unorderedPair A C) (unorderedPair B C)) (= A B))
(→ (= (unorderedPair C A) (unorderedPair C B)) (= A B))
(= (singleton A) (unorderedPair A A))
(→ (∧ (= A B) (∀ x (↔ φ ψ))) (= (separate x A φ) (separate x B ψ)))
(↔ φ ψ)(= (separate x A φ) (separate x A ψ))
(→ φ (∈ z A))(↔ (∧ (∈ B A) (subst B z φ)) (subst B z φ))
(→ φ (∈ z A))(↔ (∈ B (separate z A φ)) (subst B z φ))
(→ (= x y) (↔ φx φy))(↔ (∈ C (separate x A φx)) (∈ C (separate y A φy)))
(→ (= x y) (↔ φx φy))(= (separate x A φx) (separate y A φy))
(= (∪ A B) (⋃ (unorderedPair A B)))
(↔ (∈ A B) (∃ x (∧ (∈ A x) (= x B))))
(↔ (∈ A (∪ B C)) (∨ (∈ A B) (∈ A C)))
(→ (∈ A B) (∈ A (∪ B C)))
(→ (∈ A C) (∈ A (∪ B C)))
(= (unorderedPair A B) (∪ (singleton A) (singleton B)))
(→ (= A B) (= (⋃ A) (⋃ B)))
(= A B)(= (⋃ A) (⋃ B))
(= (∪ A A) A)
(= (⋃ (singleton A)) A)
(↔ (∈ A B) (⊆ (singleton A) B))
(→ (⊆ A B) (→ (∈ C A) (∈ C B)))
(→ (∧ (⊆ A B) (∈ B C)) (⊆ A (⋃ C)))
(→ (∈ A B) (⊆ A (⋃ B)))
(⊆ A (∪ A B))
(→ (⊆ A B) (⊆ A (∪ B C)))
(→ (∧ (∈ A C) (∈ B C)) (⊆ (unorderedPair A B) C))
(→ (⊆ (unorderedPair A B) C) (∧ (∈ A C) (∈ B C)))
(↔ (∧ (∈ A C) (∈ B C)) (⊆ (unorderedPair A B) C))
(→ (= B0 B1) (↔ (⊆ A B0) (⊆ A B1)))
(→ (= A0 A1) (↔ (⊆ A0 B) (⊆ A1 B)))
(= B0 B1)(↔ (⊆ A B0) (⊆ A B1))
(= A0 A1)(↔ (⊆ A0 B) (⊆ A1 B))