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

Theorem dfcleq 2381
Description: The same as df-cleq 2380 with the hypothesis removed using the Axiom of Extensionality ax-ext 2368. (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 2368 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2380 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 1717
This theorem is referenced by:  cvjust  2382  eqriv  2384  eqrdv  2385  eqcom  2389  eqeq1  2393  eleq2  2448  cleqh  2484  abbi  2497  nfeq  2530  nfeqd  2537  cleqf  2547  eqss  3306  ssequn1  3460  eqv  3586  disj3  3615  undif4  3627  vprc  4282  inex1  4285  axpr  4343  zfpair2  4345  sucel  4595  uniex2  4644  nbcusgra  21338  cusgrauvtxb  21371  brtxpsd3  25460  hfext  25838  onsuct0  25905  cover2  26106  undif3VD  28335  bnj145  28432
This theorem was proved from axioms:  ax-ext 2368
This theorem depends on definitions:  df-cleq 2380
  Copyright terms: Public domain W3C validator