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

Theorem dfcleq 2290
Description: The same as df-cleq 2289 with the hypothesis removed using the Axiom of Extensionality ax-ext 2277. (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 2277 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2289 1  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1530    = wceq 1632    e. wcel 1696
This theorem is referenced by:  cvjust  2291  eqriv  2293  eqrdv  2294  eqcom  2298  eqeq1  2302  eleq2  2357  cleqh  2393  abbi  2406  nfeq  2439  nfeqd  2446  cleqf  2456  eqss  3207  ssequn1  3358  eqv  3483  disj3  3512  undif4  3524  vprc  4168  inex1  4171  axpr  4229  zfpair2  4231  sucel  4481  uniex2  4531  brtxpsd3  24507  hfext  24885  onsuct0  24952  difeqri2  25143  domrngref  25163  isconcl7a  26208  cover2  26461  compneOLD  27746  nbcusgra  28298  cusgrauvtx  28309  undif3VD  28974  bnj145  29071
This theorem was proved from axioms:  ax-ext 2277
This theorem depends on definitions:  df-cleq 2289
  Copyright terms: Public domain W3C validator