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

Theorem dfcleq 2460
Description: The same as df-cleq 2459 with the hypothesis removed using the Axiom of Extensionality ax-ext 2445. (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 2445 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2459 1  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   A.wal 1377    = wceq 1379    e. wcel 1767
This theorem was proved from axioms:  ax-ext 2445
This theorem depends on definitions:  df-cleq 2459
This theorem is referenced by:  cvjust  2461  eqriv  2463  eqrdv  2464  eqeq1d  2469  eqeq1dALT  2470  eqeq1OLD  2472  eqcomOLD  2477  eleq2d  2537  eleq2dALT  2538  eleq2OLD  2542  cleqh  2582  cleqhOLD  2583  abbiOLD  2599  nfeqd  2636  nfeqOLD  2641  cleqfOLD  2657  eqss  3524  ssequn1  3679  eqv  3806  disj3  3876  undif4  3888  vprc  4591  inex1  4594  axpr  4691  zfpair2  4693  sucel  4957  fnsnb  6091  uniex2  6590  nbcusgra  24286  cusgrauvtxb  24319  brtxpsd3  29473  hfext  29767  onsuct0  29833  cover2  30131  iccshift  31445  iocopn  31447  iooshift  31449  icoopn  31452  limcdm0  31483  limcresiooub  31507  limcresioolb  31508  fperdvper  31571  itgiccshift  31621  itgperiod  31622  fourierdlem32  31762  fourierdlem33  31763  fourierdlem48  31778  fourierdlem49  31779  fourierdlem81  31811  undif3VD  33163  bnj145OLD  33263  bj-cleqh  33840  bj-abbi  33843  eliminable2a  33898  eliminable2b  33899  eliminable2c  33900  bj-ax9  33946  bj-df-cleq  33947  bj-sbeq  33950  bj-sbceqgALT  33951  bj-snsetex  34003  bj-df-v  34065
  Copyright terms: Public domain W3C validator