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

Theorem dfcleq 2499
Description: The same as df-cleq 2498 with the hypothesis removed using the Axiom of Extensionality ax-ext 2485. (Contributed by NM, 15-Sep-1993.)
Assertion
Ref Expression
dfcleq (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfcleq
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-ext 2485 . 2 (∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)
21df-cleq 2498 1 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 191  wal 1466   = wceq 1468  wcel 1937
This theorem was proved from axioms:  ax-ext 2485
This theorem depends on definitions:  df-cleq 2498
This theorem is referenced by:  cvjust  2500  eqriv  2502  eqrdv  2503  eqeq1d  2507  eqeq1dALT  2508  eleq2d  2568  eleq2dOLD  2569  eleq2dALT  2570  cleqh  2606  nfeqd  2653  eqss  3469  ssequn1  3631  eqv  3774  disj3  3849  undif4  3861  vprc  4574  inex1  4577  axpr  4679  zfpair2  4681  sucel  5547  uniex2  6662  nbcusgra  25352  cusgrauvtxb  25385  bnj145OLD  29688  brtxpsd3  30814  hfext  31101  onsuct0  31250  bj-abbi  31572  eliminable2a  31633  eliminable2b  31634  eliminable2c  31635  bj-ax9  31682  bj-df-cleq  31684  bj-sbeq  31687  bj-sbceqgALT  31688  bj-snsetex  31743  bj-df-v  31806  cover2  32278  rp-fakeinunass  36400  intimag  36487  relexp0eq  36532  undif3VD  37627  dfcleqf  37772  rnmptpr  37805  dvnmul  38237  dvnprodlem3  38242  sge00  38664  sge0resplit  38694  sge0fodjrnlem  38704  hspdifhsp  38901
  Copyright terms: Public domain W3C validator