MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cleqf Unicode version

Theorem cleqf 2443
Description: Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
Hypotheses
Ref Expression
cleqf.1  |-  F/_ x A
cleqf.2  |-  F/_ x B
Assertion
Ref Expression
cleqf  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )

Proof of Theorem cleqf
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2277 . 2  |-  ( A  =  B  <->  A. y
( y  e.  A  <->  y  e.  B ) )
2 nfv 1605 . . 3  |-  F/ y ( x  e.  A  <->  x  e.  B )
3 cleqf.1 . . . . 5  |-  F/_ x A
43nfcri 2413 . . . 4  |-  F/ x  y  e.  A
5 cleqf.2 . . . . 5  |-  F/_ x B
65nfcri 2413 . . . 4  |-  F/ x  y  e.  B
74, 6nfbi 1772 . . 3  |-  F/ x
( y  e.  A  <->  y  e.  B )
8 eleq1 2343 . . . 4  |-  ( x  =  y  ->  (
x  e.  A  <->  y  e.  A ) )
9 eleq1 2343 . . . 4  |-  ( x  =  y  ->  (
x  e.  B  <->  y  e.  B ) )
108, 9bibi12d 312 . . 3  |-  ( x  =  y  ->  (
( x  e.  A  <->  x  e.  B )  <->  ( y  e.  A  <->  y  e.  B
) ) )
112, 7, 10cbval 1924 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  <->  A. y ( y  e.  A  <->  y  e.  B ) )
121, 11bitr4i 243 1  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1527    = wceq 1623    e. wcel 1684   F/_wnfc 2406
This theorem is referenced by:  abid2f  2444  n0f  3463  iunab  3948  iinab  3963  sniota  5246  mbfposr  19007  mbfinf  19020  itg1climres  19069  eqriv2  24947  sgplpte21a  26133  compab  27644  rfcnpre1  27690  rfcnpre2  27702  bnj1366  28862
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408
  Copyright terms: Public domain W3C validator