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

Theorem dfcleq 2250
Description: The same as df-cleq 2249 with the hypothesis removed using the Axiom of Extensionality ax-ext 2237. (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 2237 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2249 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  2251  eqriv  2253  eqrdv  2254  eqcom  2258  eqeq1  2262  eleq2  2317  cleqh  2353  abbi  2366  nfeq  2399  nfeqd  2406  cleqf  2416  eqss  3155  ssequn1  3306  eqv  3431  disj3  3460  undif4  3472  vprc  4112  inex1  4115  axpr  4171  zfpair2  4173  sucel  4423  uniex2  4473  brtxpsd3  23798  hfext  24174  onsuct0  24241  difeqri2  24392  domrngref  24412  isconcl7a  25458  cover2  25711  compneOLD  26997  undif3VD  27692  bnj145  27788
This theorem was proved from axioms:  ax-ext 2237
This theorem depends on definitions:  df-cleq 2249
  Copyright terms: Public domain W3C validator