Higher-Order Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HOLE Home  >  Th. List  >  axext Unicode version

Theorem axext 219
 Description: Axiom of Extensionality. An axiom of Zermelo-Fraenkel set theory. It states that two sets are identical if they contain the same elements. Axiom Ext of [BellMachover] p. 461. (Contributed by Mario Carneiro, 10-Oct-2014.)
Hypotheses
Ref Expression
axext.1
axext.2
Assertion
Ref Expression
axext
Distinct variable groups:   ,   ,   ,

Proof of Theorem axext
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 axext.1 . . . . . 6
2 wv 64 . . . . . 6
31, 2wc 50 . . . . 5
43wl 66 . . . 4
5 axext.2 . . . . . . . 8
65, 2wc 50 . . . . . . 7
73, 6weqi 76 . . . . . 6
87ax4 150 . . . . 5
9 wal 134 . . . . . 6
107wl 66 . . . . . 6
11 wv 64 . . . . . 6
129, 11ax-17 105 . . . . . 6
137, 11ax-hbl1 103 . . . . . 6
149, 10, 11, 12, 13hbc 110 . . . . 5
153, 8, 14leqf 181 . . . 4
1615ax-cb1 29 . . . . 5
171eta 178 . . . . 5
1816, 17a1i 28 . . . 4
195eta 178 . . . . 5
2016, 19a1i 28 . . . 4
214, 15, 18, 203eqtr3i 97 . . 3
22 wtru 43 . . 3