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

Theorem dfcleq 2430
Description: The same as df-cleq 2429 with the hypothesis removed using the Axiom of Extensionality ax-ext 2417. (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 2417 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2429 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  2431  eqriv  2433  eqrdv  2434  eqcom  2438  eqeq1  2442  eleq2  2497  cleqh  2533  abbi  2546  nfeq  2579  nfeqd  2586  cleqf  2596  eqss  3363  ssequn1  3517  eqv  3643  disj3  3672  undif4  3684  vprc  4341  inex1  4344  axpr  4402  zfpair2  4404  sucel  4654  uniex2  4704  nbcusgra  21472  cusgrauvtxb  21505  brtxpsd3  25741  hfext  26124  onsuct0  26191  cover2  26415  undif3VD  28994  bnj145  29094
This theorem was proved from axioms:  ax-ext 2417
This theorem depends on definitions:  df-cleq 2429
  Copyright terms: Public domain W3C validator