# List of theorems

List of theorems in general/Relations.gh:

(= (orderedPair A B) (unorderedPair (singleton A) (unorderedPair A B)))
(→ (∧ (= A0 A1) (= B0 B1)) (= (orderedPair A0 B0) (orderedPair A1 B1)))
(→ (= B0 B1) (= (orderedPair A B0) (orderedPair A B1)))
(→ antecedent (= B0 B1))(→ antecedent (= (orderedPair A B0) (orderedPair A B1)))
(→ (= A0 A1) (= (orderedPair A0 B) (orderedPair A1 B)))
(→ antecedent (= A0 A1))(→ antecedent (= (orderedPair A0 B) (orderedPair A1 B)))
(∈ (singleton A) (orderedPair A B))
(↔ (∈ A (orderedPair B C)) (∨ (= A (singleton B)) (= A (unorderedPair B C))))
(→ (= (orderedPair A B) (orderedPair C D)) (= A C))
(→ (= (orderedPair C D) (orderedPair C B)) (= D B))
(→ (= (orderedPair A B) (orderedPair C D)) (→ (= A C) (= D B)))
(→ (= (orderedPair A B) (orderedPair C D)) (= B D))
(→ (= (orderedPair A0 B0) (orderedPair A1 B1)) (∧ (= A0 A1) (= B0 B1)))
(↔ (= (orderedPair A0 B0) (orderedPair A1 B1)) (∧ (= A0 A1) (= B0 B1)))
(↔ (relation A) (∀ z (→ (∈ z A) (∃ x (∃ y (= z (orderedPair x y)))))))
(↔ (relates A R B) (∈ (orderedPair A B) R))
(= (domain R) (separate x (⋃ (⋃ R)) (∃ y (∈ (orderedPair x y) R))))
(→ (∈ (orderedPair A B) R) (∈ (unorderedPair A B) (⋃ R)))
(→ (∃ y (∈ (orderedPair A y) R)) (∈ A (⋃ (⋃ R))))
(↔ (∈ B (domain R)) (∃ y (∈ (orderedPair B y) R)))
(→ (= R S) (= (domain R) (domain S)))
(↔ (∃ y (∈ (orderedPair C y) (singleton (orderedPair A B)))) (= C A))
(= (domain (singleton (orderedPair A B))) (singleton A))
(= (range R) (separate y (⋃ (⋃ R)) (∃ x (∈ (orderedPair x y) R))))
(→ (∃ x (∈ (orderedPair x A) R)) (∈ A (⋃ (⋃ R))))
(↔ (∈ B (range R)) (∃ x (∈ (orderedPair x B) R)))
(→ (= R S) (= (range R) (range S)))
(↔ (∃ x (∈ (orderedPair x C) (singleton (orderedPair A B)))) (= C B))
(= (range (singleton (orderedPair A B))) (singleton B))
(= (1st C) (⋃ (domain (singleton C))))
(→ (= A B) (= (1st A) (1st B)))
(= (1st (orderedPair A B)) A)
(= (2nd C) (⋃ (range (singleton C))))
(→ (= A B) (= (2nd A) (2nd B)))
(= (2nd (orderedPair A B)) B)
(= (× A B) (separate z (power (power (∪ A B))) (∃ a (∃ b (∧ (= z (orderedPair a b)) (∧ (∈ a A) (∈ b B)))))))
(→ (∧ (∈ α A) (∈ β B)) (∈ (orderedPair α β) (power (power (∪ A B)))))
(→ (∃ a (∃ b (∧ (= Z (orderedPair a b)) (∧ (∈ a A) (∈ b B))))) (∈ Z (power (power (∪ A B)))))
(↔ (∈ C (× A B)) (∃ a (∃ b (∧ (= C (orderedPair a b)) (∧ (∈ a A) (∈ b B))))))
(↔ (∈ (orderedPair A0 B0) (× A B)) (∧ (∈ A0 A) (∈ B0 B)))