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

Theorem dfcleq 2398
Description: The same as df-cleq 2397 with the hypothesis removed using the Axiom of Extensionality ax-ext 2385. (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 2385 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2397 1  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1546    = wceq 1649    e. wcel 1721
This theorem is referenced by:  cvjust  2399  eqriv  2401  eqrdv  2402  eqcom  2406  eqeq1  2410  eleq2  2465  cleqh  2501  abbi  2514  nfeq  2547  nfeqd  2554  cleqf  2564  eqss  3323  ssequn1  3477  eqv  3603  disj3  3632  undif4  3644  vprc  4301  inex1  4304  axpr  4362  zfpair2  4364  sucel  4614  uniex2  4663  nbcusgra  21425  cusgrauvtxb  21458  brtxpsd3  25650  hfext  26028  onsuct0  26095  cover2  26305  undif3VD  28703  bnj145  28800
This theorem was proved from axioms:  ax-ext 2385
This theorem depends on definitions:  df-cleq 2397
  Copyright terms: Public domain W3C validator