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

Theorem dfcleq 2603
Description: The same as df-cleq 2602 with the hypothesis removed using the Axiom of Extensionality ax-ext 2589. (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 2589 . 2 (∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)
21df-cleq 2602 1 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wal 1472   = wceq 1474  wcel 1976
This theorem was proved from axioms:  ax-ext 2589
This theorem depends on definitions:  df-cleq 2602
This theorem is referenced by:  cvjust  2604  eqriv  2606  eqrdv  2607  eqeq1d  2611  eqeq1dALT  2612  eleq2d  2672  eleq2dOLD  2673  eleq2dALT  2674  cleqh  2710  nfeqd  2757  eqss  3582  ssequn1  3744  disj3  3972  undif4  3986  vprc  4719  inex1  4722  axpr  4827  zfpair2  4829  sucel  5701  uniex2  6827  nbcusgra  25758  cusgrauvtxb  25790  bnj145OLD  29855  brtxpsd3  30979  hfext  31266  onsuct0  31416  bj-abbi  31769  eliminable2a  31830  eliminable2b  31831  eliminable2c  31832  bj-ax9  31879  bj-df-cleq  31881  bj-sbeq  31884  bj-sbceqgALT  31885  bj-snsetex  31940  bj-df-v  32003  cover2  32474  rp-fakeinunass  36676  intimag  36763  relexp0eq  36808  ntrneik4w  37214  undif3VD  37936  dfcleqf  38077  rnmptpr  38149  dvnmul  38630  dvnprodlem3  38635  sge00  39066  sge0resplit  39096  sge0fodjrnlem  39106  hspdifhsp  39303  smfresal  39470
  Copyright terms: Public domain W3C validator