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

Theorem dfcleq 2280
Description: The same as df-cleq 2279 with the hypothesis removed using the Axiom of Extensionality ax-ext 2267. (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
Dummy variables  y  z are mutually distinct and distinct from all other variables.

Proof of Theorem dfcleq
StepHypRef Expression
1 ax-ext 2267 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2279 1  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   A.wal 1529    = wceq 1625    e. wcel 1687
This theorem is referenced by:  cvjust  2281  eqriv  2283  eqrdv  2284  eqcom  2288  eqeq1  2292  eleq2  2347  cleqh  2383  abbi  2396  nfeq  2429  nfeqd  2436  cleqf  2446  eqss  3197  ssequn1  3348  eqv  3473  disj3  3502  undif4  3514  vprc  4155  inex1  4158  axpr  4214  zfpair2  4216  sucel  4466  uniex2  4516  brtxpsd3  23846  hfext  24222  onsuct0  24289  difeqri2  24440  domrngref  24460  isconcl7a  25506  cover2  25759  compneOLD  27044  undif3VD  27928  bnj145  28024
This theorem was proved from axioms:  ax-ext 2267
This theorem depends on definitions:  df-cleq 2279
  Copyright terms: Public domain W3C validator