# List of theorems

List of theorems in peano_new/set.gh:

(<-> (e. x S) (e. x T))(=_ S T)
seqid Set equality is reflexive # <title> Reflexive Property </title>
(=_ S S)
seqcom # <title> Commutative Property of Set Equality </title> # <table> # (<-> (=_ <r> S <g> T) (=_ <g> T <r> S)) # </table> # <suggest> right('Commute', '=') </suggest>
(<-> (=_ S T) (=_ T S))
seqcomi # <title> Commutative Property of Set Equality </title> # <table> # (=_ <r> S <g> T) # (=_ <g> T <r> S) # </table>
(=_ S T)(=_ T S)
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
ImpReplaceBi1Al1 # <title> Substitution </title> # <table> # (<-> ph (A. x [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (<-> ph (A. x [ [ [ ch ] )) # </table>
(<-> ph (A. x ps)) , (-> ps ch)(-> ph (A. x ch))
seqtr # <title> Transitive Property </title> # <suggest> right('Transitive', '=') </suggest>
(-> (/\ (=_ S T) (=_ T U)) (=_ S U))
eleq1i # <title> Equivalence over Element Of </title> # <table> # (= A ] ] [ B ] ) # (<-> (e. A ] S) ] [ (e. B ] S)) # </table>
(= A B)(<-> (e. A S) (e. B S))
(-> ph (= A B))(-> ph (<-> (e. A S) (e. B S)))
(-> (=_ S T) (<-> (e. A S) (e. A T)))
elseq2i # <title> Equivalence over Element Of </title> # <table> # (=_ [ S ] [ [ T ) # (<-> (e. A [ S) ] [ (e. A [ T )) # </table>
(=_ S T)(<-> (e. A S) (e. A T))
(-> ph (=_ S T))(-> ph (<-> (e. A S) (e. A T)))
BiReplaceImp1Imp1Ex1An1An0 # <title> Substitution </title> # <table> # (-> ph (-> ps (E. x (/\ ch (/\ [ th ] ] ] et))))) # (<-> [ th ] [ ta ] ) # (-> ph (-> ps (E. x (/\ ch (/\ [ [ [ ta ] et))))) # </table>
(-> ph (-> ps (E. x (/\ ch (/\ th et))))) , (<-> th ta)(-> ph (-> ps (E. x (/\ ch (/\ ta et)))))
BiReplaceImp1Imp1Ex1An0 # <title> Substitution </title> # <table> # (-> ph (-> ps (E. x (/\ [ ch ] ] ] ta)))) # (<-> [ ch ] [ th ] ) # (-> ph (-> ps (E. x (/\ [ [ [ th ] ta)))) # </table>
(-> ph (-> ps (E. x (/\ ch ta)))) , (<-> ch th)(-> ph (-> ps (E. x (/\ th ta))))
BiReplaceImp1Imp1Ex1An1An0Not0 # <title> Substitution </title> # <table> # (-> ph (-> ps (E. x (/\ ch (/\ (-. [ th ] ] ] ) et))))) # (<-> [ th ] [ ta ] ) # (-> ph (-> ps (E. x (/\ ch (/\ (-. [ [ [ ta ] ) et))))) # </table>
(-> ph (-> ps (E. x (/\ ch (/\ (-. th) et))))) , (<-> th ta)(-> ph (-> ps (E. x (/\ ch (/\ (-. ta) et)))))
BiReplaceImp1Imp1Ex1An1An1 # <title> Substitution </title> # <table> # (-> ph (-> ps (E. x (/\ ch (/\ th [ ta ] ] ] ))))) # (<-> [ ta ] [ et ] ) # (-> ph (-> ps (E. x (/\ ch (/\ th [ [ [ et ] ))))) # </table>
(-> ph (-> ps (E. x (/\ ch (/\ th ta))))) , (<-> ta et)(-> ph (-> ps (E. x (/\ ch (/\ th et)))))
ImpReplaceBi1Ex1 # <title> Substitution </title> # <table> # (<-> ph (E. x [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (<-> ph (E. x [ [ [ ch ] )) # </table>
(<-> ph (E. x ps)) , (-> ps ch)(-> ph (E. x ch))
(rwff x ph)(<-> (e. x ({|} x ph)) ph)
(-> (= x A) (<-> ph ps))(<-> (e. A ({|} x ph)) ps)
(-> (= x A) (<-> ph ps)) , (=_ S ({|} x ph))(<-> (e. A S) ps)
elabid # <title> Remove Set Abstraction </title> # <suggest> left('Simplify', '{|}') </suggest>
(<-> (e. x ({|} x (e. x S))) (e. x S))
removeab # <suggest> right('Simplify', '{|}') </suggest>
(=_ ({|} x (e. x S)) S)
elin # <title> Element in intersection is in both sets </title> # <suggest> right('Distribute', 'R') left('Distribute', '-R') </suggest>
(<-> (e. A (i^i S T)) (/\ (e. A S) (e. A T)))
elun # <title> An element of a union is in one of the sets </title> # <suggest> right('Distribute, 'R') left('Distribute', '-R') </suggest>
(<-> (e. A (u. S T)) (\/ (e. A S) (e. A T)))
(-> (e. A S) (e. A (u. S T)))
BiReplaceBi1An1 # <title> Substitution </title> # <table> # (<-> ph (/\ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (<-> ph (/\ ps [ [ [ th ] )) # </table>
(<-> ph (/\ ps ch)) , (<-> ch th)(<-> ph (/\ ps th))
BiReplaceBi1Al1 # <title> Substitution </title> # <table> # (<-> ph (A. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (A. x [ [ [ ch ] )) # </table>
(<-> ph (A. x ps)) , (<-> ps ch)(<-> ph (A. x ch))
dfss2 Problem: this theorem verified, but is not true, without constraints (S x) (T x). Consider S = {x + 1}, T = {x + 2}. The problem was that df-seq lacked these constraints, but needs them. Fixed.
(<-> (C_ S T) (A. x (-> (e. x S) (e. x T))))
BiReplaceBi1Al1Imp0 # <title> Substitution </title> # <table> # (<-> ph (A. x (-> [ ps ] ] ] th))) # (<-> [ ps ] [ ch ] ) # (<-> ph (A. x (-> [ [ [ ch ] th))) # </table>
(<-> ph (A. x (-> ps th))) , (<-> ps ch)(<-> ph (A. x (-> ch th)))
BiReplaceBi1Al1Imp1 # <title> Substitution </title> # <table> # (<-> ph (A. x (-> ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (<-> ph (A. x (-> ps [ [ [ th ] ))) # </table>
(<-> ph (A. x (-> ps ch))) , (<-> ch th)(<-> ph (A. x (-> ps th)))
(rwff x ph) , (rwff x ps)(<-> (C_ ({|} x ph) ({|} x ps)) (A. x (-> ph ps)))
BiReplaceBi1Al1Bi1 # <title> Substitution </title> # <table> # (<-> ph (A. x (<-> ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (<-> ph (A. x (<-> ps [ [ [ th ] ))) # </table>
(<-> ph (A. x (<-> ps ch))) , (<-> ch th)(<-> ph (A. x (<-> ps th)))
BiReplaceBi1Al1Bi0 # <title> Substitution </title> # <table> # (<-> ph (A. x (<-> [ ps ] ] ] th))) # (<-> [ ps ] [ ch ] ) # (<-> ph (A. x (<-> [ [ [ ch ] th))) # </table>
(<-> ph (A. x (<-> ps th))) , (<-> ps ch)(<-> ph (A. x (<-> ch th)))
abeq # <title> Alpha conversion for set abstraction </title>
(-> (= x y) (<-> ph ps))(=_ ({|} x ph) ({|} y ps))
abbi2 # <title> Equality theorem for set abstraction </title> # <suggest> right('Infer', '{|}') </suggest>
(-> (A. x (<-> ph ps)) (=_ ({|} x ph) ({|} x ps)))
BiReplaceImp1Bi0 # <title> Substitution </title> # <table> # (-> ph (<-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (<-> [ [ [ ch ] th)) # </table>
(-> ph (<-> ps th)) , (<-> ps ch)(-> ph (<-> ch th))
BiReplaceImp1Bi1 # <title> Substitution </title> # <table> # (-> ph (<-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (<-> ps [ [ [ th ] )) # </table>
(-> ph (<-> ps ch)) , (<-> ch th)(-> ph (<-> ps th))
abbi2i # <title> Equivalence over set abstraction </title> # <table> # (<-> [ ph ] [ [ ps ) # (=_ ({|} x [ ph) ] [ ({|} x [ ps )) # </table>
(<-> ph ps)(=_ ({|} x ph) ({|} x ps))
(-> (=_ S U) (<-> (=_ S T) (=_ U T)))
seqseq2 # <title> Equivalence for =_ </title> ##
(-> (=_ T U) (<-> (=_ S T) (=_ S U)))
(-> ph (=_ S U))(-> ph (<-> (=_ S T) (=_ U T)))
seqseq12 # <title> Equivalence for =_ </title> ##
(-> (/\ (=_ S T) (=_ U V)) (<-> (=_ S U) (=_ T V)))
(-> ph (=_ T U))(-> ph (<-> (=_ S T) (=_ S U)))
(-> ph (=_ S T)) , (-> ph (=_ U V))(-> ph (<-> (=_ S U) (=_ T V)))
(=_ S T)(<-> (=_ S U) (=_ T U))
(=_ S T)(<-> (=_ U S) (=_ U T))
BiReplaceSeq1Ab1 # <title> Substitution </title> # <table> # (=_ S ({|} x [ ph ] ] ] )) # (<-> [ ph ] [ ps ] ) # (=_ S ({|} x [ [ [ ps ] )) # </table>
(=_ S ({|} x ph)) , (<-> ph ps)(=_ S ({|} x ps))
df-emptysetF # <title> Definition of Empty Set </suggest> # <suggest> left('Simplify', '∅') right('Define', '∅') </suggest>
(=_ ({/}) ({|} x (F)))
BiReplaceImp1Not0 # <title> Substitution </title> # <table> # (-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (-. [ [ [ ch ] )) # </table>
(-> ph (-. ps)) , (<-> ps ch)(-> ph (-. ch))
noel # <title> Empty Set Contains No Elements </title>
(-. (e. A ({/})))
notEmpty # <title> A set with an element is not empty </title>
(-> (e. A S) (-. (=_ S ({/}))))
elsnc # <title> Singleton has One Element </title> # <suggest> right('Simplify', '=') </suggest>
(<-> (e. A ({} B)) (= A B))
snid # <title> Singleton has One Element </title>
(e. A ({} A))
elSubset # <title> Subset and Element Of Equivalence <title> # <suggest> left('Simplify', '∈') right('Infer', '⊆') </suggest>
(<-> (e. A S) (C_ ({} A) S))
elSubseti # <title> Subset and Element Of Equivalence <title>
(e. A S)(C_ ({} A) S)
abbi2d # <title> Equality deduction for set abstraction </title>
(-> ph (<-> ps ch))(-> ph (=_ ({|} x ps) ({|} x ch)))
SeqReplaceSeq0 # <title> Substitution </title> # <table> # (=_ [ S ] ] ] U) # (=_ [ S ] [ T ] ) # (=_ [ [ [ T ] U) # </table>
(=_ S U) , (=_ S T)(=_ T U)
SeqReplaceImp1Seq0 # <title> Substitution </title> # <table> # (-> ph (=_ [ S ] ] ] U)) # (=_ [ S ] [ T ] ) # (-> ph (=_ [ [ [ T ] U)) # </table>
(-> ph (=_ S U)) , (=_ S T)(-> ph (=_ T U))
SeqReplaceImp1Seq1 # <title> Substitution </title> # <table> # (-> ph (=_ S [ T ] ] ] )) # (=_ [ T ] [ U ] ) # (-> ph (=_ S [ [ [ U ] )) # </table>
(-> ph (=_ S T)) , (=_ T U)(-> ph (=_ S U))
(-> (= A B) (=_ ({} A) ({} B)))
(= A B)(=_ ({} A) ({} B))
SeqReplaceSeq1 # <title> Substitution </title> # <table> # (=_ S [ T ] ] ] ) # (=_ [ T ] [ U ] ) # (=_ S [ [ [ U ] ) # </table>
(=_ S T) , (=_ T U)(=_ S U)
SeqReplacerSeq0Ab1Or0El0 # <title> Substitution </title> # <table> # (=_ U ({|} x (\/ (e. A [ S ] ] ] ) ph))) # (=_ [ S ] [ T ] ) # (=_ U ({|} x (\/ (e. A [ [ [ T ] ) ph))) # </table>
(=_ U ({|} x (\/ (e. A S) ph))) , (=_ S T)(=_ U ({|} x (\/ (e. A T) ph)))
(-. ph)(=_ ({|} x ph) ({/}))
(-> (=_ S U) (=_ (u. S T) (u. U T)))
(=_ S U)(=_ (u. S T) (u. U T))
unseq2 # <title> Equivalence for u. </title> ##
(-> (=_ T U) (=_ (u. S T) (u. S U)))
(-> ph (=_ S U))(-> ph (=_ (u. S T) (u. U T)))
(=_ T U)(=_ (u. S T) (u. S U))
unseq12 # <title> Equivalence for u. </title> ##
(-> (/\ (=_ S T) (=_ U V)) (=_ (u. S U) (u. T V)))
(-> ph (=_ T U))(-> ph (=_ (u. S T) (u. S U)))
(-> ph (=_ S T)) , (-> ph (=_ U V))(-> ph (=_ (u. S U) (u. T V)))
SeqReplaceSeq0Ab1An0El0 # <title> Substitution </title> # <table> # (=_ U ({|} x (/\ (e. A [ S ] ] ] ) ph))) # (=_ [ S ] [ T ] ) # (=_ U ({|} x (/\ (e. A [ [ [ T ] ) ph))) # </table>
(=_ U ({|} x (/\ (e. A S) ph))) , (=_ S T)(=_ U ({|} x (/\ (e. A T) ph)))
inseq1 # <title> Equivalence over Intersection </title>
(-> (=_ S T) (=_ (i^i S U) (i^i T U)))
(=_ S T)(=_ (i^i S U) (i^i T U))
inseq2 # <title> Equivalence for ∩ </title> ##
(-> (=_ T U) (=_ (i^i S T) (i^i S U)))
(-> ph (=_ S T))(-> ph (=_ (i^i S U) (i^i T U)))
(=_ T U)(=_ (i^i S T) (i^i S U))
(-> ph (=_ T U))(-> ph (=_ (i^i S T) (i^i S U)))
SeqReplaceSeq0Ab1An1El0 # <title> Substitution </title> # <table> # (=_ U ({|} x (/\ ph (e. A [ S ] ] ] )))) # (=_ [ S ] [ T ] ) # (=_ U ({|} x (/\ ph (e. A [ [ [ T ] )))) # </table>
(=_ U ({|} x (/\ ph (e. A S)))) , (=_ S T)(=_ U ({|} x (/\ ph (e. A T))))
SeqReplaceBi0Seq0In0 # <title> Substitution </title> # <table> # (<-> (=_ (i^i [ S ] ] ] U) V) ph) # (=_ [ S ] [ T ] ) # (<-> (=_ (i^i [ [ [ T ] U) V) ph) # </table>
(<-> (=_ (i^i S U) V) ph) , (=_ S T)(<-> (=_ (i^i T U) V) ph)
SeqReplaceBi0Seq1 # <title> Substitution </title> # <table> # (<-> (=_ S [ T ] ] ] ) ph) # (=_ [ T ] [ U ] ) # (<-> (=_ S [ [ [ U ] ) ph) # </table>
(<-> (=_ S T) ph) , (=_ T U)(<-> (=_ S U) ph)
ssseq1 # <title> Equivalence for C_ </title> ##
(-> (=_ S U) (<-> (C_ S T) (C_ U T)))
(=_ S U)(<-> (C_ S T) (C_ U T))
ssseq2 # <title> Equivalence for C_ </title> ##
(-> (=_ T U) (<-> (C_ S T) (C_ S U)))
(-> ph (=_ S U))(-> ph (<-> (C_ S T) (C_ U T)))
(=_ T U)(<-> (C_ S T) (C_ S U))
ssseq12 # <title> Equivalence for C_ </title> ##
(-> (/\ (=_ S T) (=_ U V)) (<-> (C_ S U) (C_ T V)))
(-> ph (=_ T U))(-> ph (<-> (C_ S T) (C_ S U)))
(-> ph (=_ S T)) , (-> ph (=_ U V))(-> ph (<-> (C_ S U) (C_ T V)))
SeqReplaceBi0Seq0In1 # <title> Substitution </title> # <table> # (<-> (=_ (i^i S [ T ] ] ] ) V) ph) # (=_ [ T ] [ U ] ) # (<-> (=_ (i^i S [ [ [ U ] ) V) ph) # </table>
(<-> (=_ (i^i S T) V) ph) , (=_ T U)(<-> (=_ (i^i S U) V) ph)
uncom # <title> Commutative Property of Union </title> # <suggest> right('Commute', '∪') </suggest>
(=_ (u. S T) (u. T S))
incom # <title> Commutative Property of Intersection </title> # <suggest> right('Commute', '∩') </suggest>
(=_ (i^i S T) (i^i T S))
BiReplaceBi1An0 # <title> Substitution </title> # <table> # (<-> ph (/\ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (/\ [ [ [ ch ] th)) # </table>
(<-> ph (/\ ps th)) , (<-> ps ch)(<-> ph (/\ ch th))
BiReplaceBi1Or0 # <title> Substitution </title> # <table> # (<-> ph (\/ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (\/ [ [ [ ch ] th)) # </table>
(<-> ph (\/ ps th)) , (<-> ps ch)(<-> ph (\/ ch th))
BiReplaceBi1Or1 # <title> Substitution </title> # <table> # (<-> ph (\/ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (<-> ph (\/ ps [ [ [ th ] )) # </table>
(<-> ph (\/ ps ch)) , (<-> ch th)(<-> ph (\/ ps th))
inass # <title> Associative Property </title> # <suggest> right('Associate', 'R') left('Associate', 'L') </suggest>
(=_ (i^i (i^i S T) U) (i^i S (i^i T U)))
BiReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (<-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (<-> ps ch)(<-> ph ch)
unass # <title> Associative Property </title> # <suggest> right('Associate', 'R') left('Associate', 'L') </suggest>
(=_ (u. (u. S T) U) (u. S (u. T U)))
undi # <title> Distributive Property </title> # <suggest> right('Distribute', 'L') left('Distribute', '-L') </suggest>
(=_ (u. S (i^i T U)) (i^i (u. S T) (u. S U)))
undir # <title> Distributive Property </title> # <suggest> right('Distribute', 'R') left('Distribute', '-R') </suggest>
(=_ (u. (i^i T U) S) (i^i (u. T S) (u. U S)))
indir # <title> Distributive Property </title> # <suggest> right('Distribute', 'R') left('Distribute', '-R') </suggest>
(=_ (i^i (u. T U) S) (u. (i^i T S) (i^i U S)))
indi # <title> Distributive Property </title> # <suggest> right('Distribute', 'L') left('Distribute', '-L') </suggest>
(=_ (i^i S (u. T U)) (u. (i^i S T) (i^i S U)))
unionAttach1 # <summary> If an element is in a set, it is also in the set unioned with anything. </summary> # <table> # (e. A [ S ] ) # (e. A (u. [ S ] <g> U)) # </table>
(e. A S)(e. A (u. S U))
unionAttach2 # <summary> If an element is in a set, it is also in the set unioned with anything. </summary> # <table> # (e. A ] [ S) # (e. A ] (u. <g> U [ S)) # </table>
(e. A S)(e. A (u. U S))
SeqReplaceBi1Seq0 # <title> Substitution </title> # <table> # (<-> ph (=_ [ S ] ] ] U)) # (=_ [ S ] [ T ] ) # (<-> ph (=_ [ [ [ T ] U)) # </table>
(<-> ph (=_ S U)) , (=_ S T)(<-> ph (=_ T U))
SeqReplaceBi1Seq0Un0 # <title> Substitution </title> # <table> # (<-> ph (=_ (u. [ S ] ] ] U) V)) # (=_ [ S ] [ T ] ) # (<-> ph (=_ (u. [ [ [ T ] U) V)) # </table>
(<-> ph (=_ (u. S U) V)) , (=_ S T)(<-> ph (=_ (u. T U) V))
SeqReplaceBi0Ss0 # <title> Substitution </title> # <table> # (<-> (C_ [ S ] ] ] U) ph) # (=_ [ S ] [ T ] ) # (<-> (C_ [ [ [ T ] U) ph) # </table>
(<-> (C_ S U) ph) , (=_ S T)(<-> (C_ T U) ph)
SeqReplaceBi1Seq0Un1 # <title> Substitution </title> # <table> # (<-> ph (=_ (u. S [ T ] ] ] ) V)) # (=_ [ T ] [ U ] ) # (<-> ph (=_ (u. S [ [ [ U ] ) V)) # </table>
(<-> ph (=_ (u. S T) V)) , (=_ T U)(<-> ph (=_ (u. S U) V))
unSubset # <summary> If a set is a subset of two sets, it is a subset of their union. </summary>
(C_ S U) , (C_ T U)(C_ (u. S T) U)
notInUnion # <summary> If an element is not in two sets, it is not in the union of the sets. </summary>
(-. (e. A S)) , (-. (e. A T))(-. (e. A (u. S T)))
notInSingleton # <summary> Proof that an element is not in a singleton. </summary>
(-. (= A B))(-. (e. A ({} B)))
notInSingletonUnion # <summary> Proof that an element is not in the union of singleton and another set. </summary>
(-. (= A B)) , (-. (e. A S))(-. (e. A (u. ({} B) S)))
notInSingletonUnion2 # <summary> Proof that an element is not in the union of singleton and another set. </summary>
(-. (e. A S)) , (-. (= A B))(-. (e. A (u. S ({} B))))
BiReplaceImp0Not0Not0 # <title> Substitution </title> # <table> # (-> (-. (-. [ ph ] ] ] )) ch) # (<-> [ ph ] [ ps ] ) # (-> (-. (-. [ [ [ ps ] )) ch) # </table>
(-> (-. (-. ph)) ch) , (<-> ph ps)(-> (-. (-. ps)) ch)
emptyIn1 # <title> Empty Set Intersection </title> # <suggest> auto-right('Simplify', '∅') </suggest>
(=_ (i^i ({/}) S) ({/}))
(=_ (i^i S ({/})) ({/}))
emptyss # <title> Empty Set is a Subset </title> # <suggest> full('Simplify', 'T') </suggest>
(C_ ({/}) S)
(-. (e. A S))(=_ (i^i ({} A) S) ({/}))
(-. (e. A S))(=_ (i^i S ({} A)) ({/}))
inidm # <title> Intersection is Idempotent </title> # <suggest> right('Simplify', '∩') </suggest>
(=_ (i^i S S) S)
unidm # <title> Union is Idempotent </title> # <suggest> right('Simplify', '∪') </suggest>
(=_ (u. S S) S)
(=_ (i^i S ({/})) ({/}))
(=_ (i^i ({/}) S) ({/}))
unid # <title> Union Identity </title>
(=_ (u. S ({/})) S)
unidr # <title> Union Identity </title>
(=_ (u. ({/}) S) S)
BiReplaceImp1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (E. x [ [ [ ch ] )) # </table>
(-> ph (E. x ps)) , (<-> ps ch)(-> ph (E. x ch))
ImpReplaceEx1 # <title> Substitution </title> # <table> # (E. x [ ph ] ] ] ) # (-> [ ph ] [ ps ] ) # (E. x [ [ [ ps ] ) # </table>
(E. x ph) , (-> ph ps)(E. x ps)
BiReplaceBi1Not0 # <title> Substitution </title> # <table> # (<-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. [ [ [ ch ] )) # </table>
(<-> ph (-. ps)) , (<-> ps ch)(<-> ph (-. ch))
BiReplaceBi1Not0Or1 # <title> Substitution </title> # <table> # (<-> ph (-. (\/ ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (<-> ph (-. (\/ ps [ [ [ th ] ))) # </table>
(<-> ph (-. (\/ ps ch))) , (<-> ch th)(<-> ph (-. (\/ ps th)))
BiReplaceBi1Imp0 # <title> Substitution </title> # <table> # (<-> ph (-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (-> [ [ [ ch ] th)) # </table>
(<-> ph (-> ps th)) , (<-> ps ch)(<-> ph (-> ch th))
(-> (E. x (/\ (e. x S) (-. (e. x T)))) (-. (=_ S T)))
(<-> ([/] A x (/\ (e. x S) (-. (e. x T)))) (/\ (e. A S) (-. (e. A T))))
elnotseq # <title> Sets are not equal </title> # <suggest> right('Infer', '≠') </suggest>
(-> (/\ (e. A S) (-. (e. A T))) (-. (=_ S T)))
elnotseqcom # <title> Sets are not equal </title>
(-> (/\ (e. A S) (-. (e. A T))) (-. (=_ T S)))
(e. A S) , (-. (e. A T))(E. x (/\ (e. x S) (-. (e. x T))))
notSeq # <title> Sets are not equal </title>
(e. A S) , (-. (e. A T))(-. (=_ S T))
(-> (E. x (/\ (e. x T) (-. (e. x S)))) (-. (=_ S T)))
notSeq2 # <title> Sets are not equal </title>
(-. (e. A S)) , (e. A T)(-. (=_ S T))
BiReplaceBi1Not0Al1 # <title> Substitution </title> # <table> # (<-> ph (-. (A. x [ ps ] ] ] ))) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. (A. x [ [ [ ch ] ))) # </table>
(<-> ph (-. (A. x ps))) , (<-> ps ch)(<-> ph (-. (A. x ch)))
(-> (E. x (/\ (e. x S) (-. (e. x T)))) (-. (C_ S T)))
BiReplaceImp1Al1 # <title> Substitution </title> # <table> # (-> ph (A. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (A. x [ [ [ ch ] )) # </table>
(-> ph (A. x ps)) , (<-> ps ch)(-> ph (A. x ch))
BiReplaceImp1Al1Not0 # <title> Substitution </title> # <table> # (-> ph (A. x (-. [ ps ] ] ] ))) # (<-> [ ps ] [ ch ] ) # (-> ph (A. x (-. [ [ [ ch ] ))) # </table>
(-> ph (A. x (-. ps))) , (<-> ps ch)(-> ph (A. x (-. ch)))
subsetnoextra # <title> Subsets cannot have additional elements </title>
(-> (/\ (C_ S T) (-. (e. A T))) (-. (e. A S)))
(C_ S S)
(=_ (i^i S (u. S T)) S)
ssUnion # <title> Subset of a Union </title>
(C_ S (u. S T))
notSs # <title> Not a Subset </title>
(e. A S) , (-. (e. A T))(-. (C_ S T))
dfpssi # <title> Combine Set Inclusions </title>
(C_ S T) , (-. (=_ S T))(C. S T)
pssSs # <title> Proper Subset Implies Subset </title> # <suggest> right('Infer', '⊆') </suggest>
(-> (C. S T) (C_ S T))
pssNeq # <title> Proper Subset Implies Inequality </title> # <suggest> right('Infer', '≠') </suggest>
(-> (C. S T) (-. (=_ S T)))
nssNpss # <title> Not Subset Implies Not Proper Subset </title> # <suggest> right('Infer', '⊄') </suggest>
(-> (-. (C_ S T)) (-. (C. S T)))
seqNpss # <title> Equality Implies Not Proper Subset </title> # <suggest> right('Infer', '⊄') </suggest>
(-> (=_ S T) (-. (C. S T)))
seqss # <title> Two equal set are also subsets </title>
(-> (=_ S T) (C_ S T))
EqReplaceEq0 # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
EqReplaceEq1 # <title> Substitution </title> # <table> # (= A [ B ] ] ] ) # (= [ B ] [ C ] ) # (= A [ [ [ C ] ) # </table>
(= A B) , (= B C)(= A C)

## Iota

(=_ S T)(= (iota S) (iota T))
(-> ph (=_ S T))(-> ph (= (iota S) (iota T)))
SeqReplaceEq1Iota0 # <title> Substitution </title> # <table> # (= A (iota [ S ] ] ] )) # (=_ [ S ] [ T ] ) # (= A (iota [ [ [ T ] )) # </table>
(= A (iota S)) , (=_ S T)(= A (iota T))
BiReplaceEq1Iota0Ab1 # <title> Substitution </title> # <table> # (= A (iota ({|} x [ ph ] ] ] ))) # (<-> [ ph ] [ ps ] ) # (= A (iota ({|} x [ [ [ ps ] ))) # </table>
(= A (iota ({|} x ph))) , (<-> ph ps)(= A (iota ({|} x ps)))
iotacl # <summary> Existential uniqueness implies iota is a member </summary>
(-> (E! x (e. x S)) (e. (iota S) S))
iotacl2 # <summary> Another iota utility theorem. Asserts that if exactly one x has the property ph, then that x can be found using iota. </summary>
(-> (E! x ph) (e. (iota ({|} x ph)) ({|} x ph)))
iotaeq # <title> Basic identity for iota </title>
(= (iota ({|} x (= x A))) A)
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)