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

Theorem axext 206
 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.
Hypotheses
Ref Expression
axext.1
axext.2
Assertion
Ref Expression
axext
Distinct variable groups:   ,   ,   ,

Proof of Theorem axext
StepHypRef Expression
1 axext.1 . . . . . 6
2 wv 58 . . . . . 6
31, 2wc 45 . . . . 5
43wl 59 . . . 4
5 axext.2 . . . . . . . 8
65, 2wc 45 . . . . . . 7
73, 6weqi 68 . . . . . 6
87ax4 140 . . . . 5
9 wal 124 . . . . . 6
107wl 59 . . . . . 6
11 wv 58 . . . . . 6
129, 11ax-17 95 . . . . . 6
137, 11ax-hbl1 93 . . . . . 6
149, 10, 11, 12, 13hbc 100 . . . . 5
153, 8, 14leqf 169 . . . 4
1615ax-cb1 29 . . . . 5
171eta 166 . . . . 5
1816, 17a1i 28 . . . 4
195eta 166 . . . . 5
2016, 19a1i 28 . . . 4
214, 15, 18, 203eqtr3i 87 . . 3
22 wtru 40 . . 3