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

Theorem dfcleq 2437
Description: The same as df-cleq 2436 with the hypothesis removed using the Axiom of Extensionality ax-ext 2423. (Contributed by NM, 15-Sep-1993.)
Assertion
Ref Expression
dfcleq  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
Distinct variable groups:    x, A    x, B

Proof of Theorem dfcleq
Dummy variables  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-ext 2423 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2436 1  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   A.wal 1367    = wceq 1369    e. wcel 1756
This theorem was proved from axioms:  ax-ext 2423
This theorem depends on definitions:  df-cleq 2436
This theorem is referenced by:  cvjust  2438  eqriv  2440  eqrdv  2441  eqcom  2445  eqeq1  2449  eleq2  2504  cleqh  2542  cleqhOLD  2543  abbiOLD  2559  nfeqd  2596  nfeqOLD  2600  cleqf  2615  eqss  3383  ssequn1  3538  eqv  3665  disj3  3735  undif4  3747  vprc  4442  inex1  4445  axpr  4542  zfpair2  4544  sucel  4804  fnsnb  5910  uniex2  6387  nbcusgra  23383  cusgrauvtxb  23416  brtxpsd3  27939  hfext  28233  onsuct0  28299  cover2  28619  undif3VD  31630  bnj145OLD  31730  bj-cleqh  32305  bj-abbi  32308  eliminable2a  32363  eliminable2b  32364  eliminable2c  32365  bj-ax9  32411  bj-df-cleq  32412  bj-sbeq  32415  bj-sbceqgALT  32416  bj-snsetex  32468
  Copyright terms: Public domain W3C validator