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

Theorem dfcleq 2429
Description: The same as df-cleq 2428 with the hypothesis removed using the Axiom of Extensionality ax-ext 2416. (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 2416 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2428 1  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1549    = wceq 1652    e. wcel 1725
This theorem is referenced by:  cvjust  2430  eqriv  2432  eqrdv  2433  eqcom  2437  eqeq1  2441  eleq2  2496  cleqh  2532  abbi  2545  nfeq  2578  nfeqd  2585  cleqf  2595  eqss  3355  ssequn1  3509  eqv  3635  disj3  3664  undif4  3676  vprc  4333  inex1  4336  axpr  4394  zfpair2  4396  sucel  4646  uniex2  4695  nbcusgra  21460  cusgrauvtxb  21493  brtxpsd3  25691  hfext  26072  onsuct0  26139  cover2  26352  undif3VD  28848  bnj145  28948
This theorem was proved from axioms:  ax-ext 2416
This theorem depends on definitions:  df-cleq 2428
  Copyright terms: Public domain W3C validator