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

Theorem dfcleq 2455
Description: The same as df-cleq 2454 with the hypothesis removed using the Axiom of Extensionality ax-ext 2441. (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 2441 . 2  |-  ( A. x ( x  e.  y  <->  x  e.  z
)  ->  y  =  z )
21df-cleq 2454 1  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189   A.wal 1452    = wceq 1454    e. wcel 1897
This theorem was proved from axioms:  ax-ext 2441
This theorem depends on definitions:  df-cleq 2454
This theorem is referenced by:  cvjust  2456  eqriv  2458  eqrdv  2459  eqeq1d  2463  eqeq1dALT  2464  eleq2d  2524  eleq2dOLD  2525  eleq2dALT  2526  cleqh  2562  nfeqd  2609  eqss  3458  ssequn1  3615  eqv  3759  disj3  3820  undif4  3832  vprc  4554  inex1  4557  axpr  4651  zfpair2  4653  sucel  5514  uniex2  6612  nbcusgra  25239  cusgrauvtxb  25272  bnj145OLD  29583  brtxpsd3  30711  hfext  30998  onsuct0  31149  bj-abbi  31434  eliminable2a  31493  eliminable2b  31494  eliminable2c  31495  bj-ax9  31542  bj-df-cleq  31544  bj-sbeq  31547  bj-sbceqgALT  31548  bj-snsetex  31601  bj-vjust2  31663  bj-df-v  31664  cover2  32084  rp-fakeinunass  36204  intimag  36292  relexp0eq  36337  undif3VD  37318  rnmptpr  37481  dvnmul  37855  dvnprodlem3  37860  sge00  38255  sge0resplit  38285  sge0fodjrnlem  38295  hspdifhsp  38475
  Copyright terms: Public domain W3C validator