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

Theorem dfcleq 2277
Description: The same as df-cleq 2276 with the hypothesis removed using the Axiom of Extensionality ax-ext 2264. (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 2264 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2276 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
This theorem is referenced by:  cvjust  2278  eqriv  2280  eqrdv  2281  eqcom  2285  eqeq1  2289  eleq2  2344  cleqh  2380  abbi  2393  nfeq  2426  nfeqd  2433  cleqf  2443  eqss  3194  ssequn1  3345  eqv  3470  disj3  3499  undif4  3511  vprc  4152  inex1  4155  axpr  4213  zfpair2  4215  sucel  4465  uniex2  4515  brtxpsd3  24436  hfext  24813  onsuct0  24880  difeqri2  25040  domrngref  25060  isconcl7a  26105  cover2  26358  compneOLD  27643  nbcusgra  28159  cusgrauvtx  28168  undif3VD  28658  bnj145  28755
This theorem was proved from axioms:  ax-ext 2264
This theorem depends on definitions:  df-cleq 2276
  Copyright terms: Public domain W3C validator