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

Theorem dfcleq 2247
Description: The same as df-cleq 2246 with the hypothesis removed using the Axiom of Extensionality ax-ext 2234. (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
StepHypRef Expression
1 ax-ext 2234 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2246 1  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   A.wal 1532    = wceq 1619    e. wcel 1621
This theorem is referenced by:  cvjust  2248  eqriv  2250  eqrdv  2251  eqcom  2255  eqeq1  2259  eleq2  2314  cleqh  2346  abbi  2359  nfeq  2392  nfeqd  2399  cleqf  2409  eqss  3115  ssequn1  3255  eqv  3377  disj3  3406  undif4  3418  vprc  4049  inex1  4052  axpr  4107  zfpair2  4109  sucel  4358  uniex2  4406  brtxpsd3  23611  hfext  23987  onsuct0  24054  difeqri2  24205  domrngref  24225  isconcl7a  25271  cover2  25524  compneOLD  26810  undif3VD  27348  bnj145  27444
This theorem was proved from axioms:  ax-ext 2234
This theorem depends on definitions:  df-cleq 2246
  Copyright terms: Public domain W3C validator