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

Theorem dfcleq 2604
Description: The same as df-cleq 2603 with the hypothesis removed using the Axiom of Extensionality ax-ext 2590. (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 2590 . 2 (∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)
21df-cleq 2603 1 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wal 1473   = wceq 1475  wcel 1977
This theorem was proved from axioms:  ax-ext 2590
This theorem depends on definitions:  df-cleq 2603
This theorem is referenced by:  cvjust  2605  eqriv  2607  eqrdv  2608  eqeq1d  2612  eqeq1dALT  2613  eleq2d  2673  eleq2dOLD  2674  eleq2dALT  2675  cleqh  2711  nfeqd  2758  eqss  3583  ssequn1  3745  disj3  3973  undif4  3987  vprc  4724  inex1  4727  axpr  4832  zfpair2  4834  sucel  5715  uniex2  6850  nbcusgra  25992  cusgrauvtxb  26024  bnj145OLD  30049  brtxpsd3  31173  hfext  31460  onsuct0  31610  bj-abbi  31963  eliminable2a  32034  eliminable2b  32035  eliminable2c  32036  bj-ax9  32083  bj-df-cleq  32085  bj-sbeq  32088  bj-sbceqgALT  32089  bj-snsetex  32144  bj-df-v  32207  cover2  32678  rp-fakeinunass  36880  intimag  36967  relexp0eq  37012  ntrneik4w  37418  undif3VD  38140  dfcleqf  38281  rnmptpr  38353  dvnmul  38833  dvnprodlem3  38838  sge00  39269  sge0resplit  39299  sge0fodjrnlem  39309  hspdifhsp  39506  smfresal  39673
  Copyright terms: Public domain W3C validator