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

Theorem dfcleq 2765
Description: The same as df-cleq 2764 with the hypothesis removed using the Axiom of Extensionality ax-ext 2751. (Contributed by NM, 15-Sep-1993.) Revised to make use of axext3 2753 instead of ax-ext 2751, so that ax-9 2154 will appear in lists of axioms used by a proof, since df-cleq 2764 implies ax-9 2154 by theorem bj-ax9 33218. We may revisit this in the future. (Revised by NM, 28-Oct-2021.) (Proof modification is discouraged.)
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 axext3 2753 . 2 (∀𝑥(𝑥𝑦𝑥𝑧) → 𝑦 = 𝑧)
21df-cleq 2764 1 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1629   = wceq 1631  wcel 2145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764
This theorem is referenced by:  cvjust  2766  eqriv  2768  eqrdv  2769  eqeq1d  2773  eqeq1dALT  2774  eleq2d  2836  eleq2dALT  2837  cleqh  2873  nfeqd  2921  eqv  3356  eqss  3767  ssequn1  3934  disj3  4165  undif4  4178  vnex  4931  inex1  4934  axpr  5034  zfpair2  5036  sucel  5940  uniex2  7102  brtxpsd3  32339  hfext  32626  onsuct0  32776  bj-abbi  33110  eliminable2a  33174  eliminable2b  33175  eliminable2c  33176  bj-df-cleq  33221  bj-sbeq  33224  bj-sbceqgALT  33225  bj-snsetex  33281  bj-df-v  33346  cover2  33839  releccnveq  34364  rp-fakeinunass  38387  intimag  38474  relexp0eq  38519  ntrneik4w  38924  undif3VD  39640  rnmptpr  39877  uzinico  40302  dvnmul  40673  dvnprodlem3  40678  sge00  41107  sge0resplit  41137  sge0fodjrnlem  41147  hspdifhsp  41347  smfresal  41512
  Copyright terms: Public domain W3C validator