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

Theorem dfcleq 2508
Description: The same as df-cleq 2507 with the hypothesis removed using the Axiom of Extensionality ax-ext 2494. (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 2494 . 2 (∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)
21df-cleq 2507 1 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wal 1472   = wceq 1474  wcel 1938
This theorem was proved from axioms:  ax-ext 2494
This theorem depends on definitions:  df-cleq 2507
This theorem is referenced by:  cvjust  2509  eqriv  2511  eqrdv  2512  eqeq1d  2516  eqeq1dALT  2517  eleq2d  2577  eleq2dOLD  2578  eleq2dALT  2579  cleqh  2615  nfeqd  2662  eqss  3487  ssequn1  3649  disj3  3876  undif4  3890  vprc  4623  inex1  4626  axpr  4731  zfpair2  4733  sucel  5603  uniex2  6725  nbcusgra  25731  cusgrauvtxb  25763  bnj145OLD  29895  brtxpsd3  31009  hfext  31296  onsuct0  31445  bj-abbi  31805  eliminable2a  31866  eliminable2b  31867  eliminable2c  31868  bj-ax9  31915  bj-df-cleq  31917  bj-sbeq  31920  bj-sbceqgALT  31921  bj-snsetex  31976  bj-df-v  32039  cover2  32553  rp-fakeinunass  36762  intimag  36849  relexp0eq  36894  ntrneik4w  37300  undif3VD  38022  dfcleqf  38164  rnmptpr  38236  dvnmul  38723  dvnprodlem3  38728  sge00  39163  sge0resplit  39193  sge0fodjrnlem  39203  hspdifhsp  39400  smfresal  39567
  Copyright terms: Public domain W3C validator