NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  bm1.1 Unicode version

Theorem bm1.1 1881
Description: Any set defined by a property is the only set defined by that property. Theorem 1.1 of [BellMachover] p. 462.
Hypothesis
Ref Expression
bm1.1.1
Assertion
Ref Expression
bm1.1
Distinct variable group:   ,
Allowed substitution hints:   (,)

Proof of Theorem bm1.1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ax-17 1413 . . . . . . . 8
2 bm1.1.1 . . . . . . . 8
31, 2hbbi 1448 . . . . . . 7
43hbal 1346 . . . . . 6
5 elequ2 1535 . . . . . . . 8
65bibi1d 307 . . . . . . 7
76albidv 1677 . . . . . 6
84, 7sbie 1592 . . . . 5
9 19.26 1371 . . . . . 6
10 biantr 847 . . . . . . . 8
1110alimi 1334 . . . . . . 7
12 ax-ext 1877 . . . . . . 7
1311, 12syl 14 . . . . . 6
149, 13sylbir 201 . . . . 5
158, 14sylan2b 452 . . . 4
1615gen2 1329 . . 3
1716jctr 517 . 2
18 ax-17 1413 . . 3
1918eu2 1810 . 2
2017, 19sylibr 200 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 173   wa 355  wal 1322  wex 1327   wceq 1398   wcel 1400  wsbc 1566  weu 1791
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1323  ax-6 1324  ax-7 1325  ax-gen 1326  ax-8 1402  ax-10 1403  ax-11 1404  ax-12 1405  ax-14 1407  ax-17 1413  ax-9 1424  ax-4 1429  ax-16 1606  ax-ext 1877
This theorem depends on definitions:  df-bi 174  df-or 356  df-an 357  df-ex 1328  df-sb 1568  df-eu 1795
  Copyright terms: Public domain W3C validator