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

Theorem dfcleq 2792
 Description: The defining characterization of class equality. It is proved, over Tarski's FOL, from the axiom of (set) extensionality (ax-ext 2770) and the definition of class equality (df-cleq 2791). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2773 to prove also the hypothesis of df-cleq 2791 that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen 1797, equid 2019 }. (Contributed by NM, 15-Sep-1993.) (Revised by BJ, 24-Jun-2019.)
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 axextb 2773 . 2 (𝑦 = 𝑧 ↔ ∀𝑢(𝑢𝑦𝑢𝑧))
2 axextb 2773 . 2 (𝑡 = 𝑡 ↔ ∀𝑣(𝑣𝑡𝑣𝑡))
31, 2df-cleq 2791 1 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209  ∀wal 1536   = wceq 1538   ∈ wcel 2111 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791 This theorem is referenced by:  cvjust  2793  ax9ALT  2794  eqriv  2795  eqrdv  2796  eqeq1d  2800  eqeq1dALT  2801  abbi  2865  eleq2d  2875  eleq2dALT  2876  cleqh  2913  nfeqd  2965  cleqf  2983  eqv  3449  dfss2  3901  eqss  3930  ssequn1  4107  eq0  4258  disj  4355  disj3  4361  undif4  4374  vnex  5182  inex1  5185  axprALT  5288  zfpair2  5296  sucel  6232  uniex2  7446  brtxpsd3  33482  hfext  33769  onsuct0  33914  eliminable2a  34314  eliminable2b  34315  eliminable2c  34316  eliminable-veqab  34320  eliminable-abeqv  34321  eliminable-abeqab  34322  bj-ax9  34356  bj-sbeq  34358  bj-sbceqgALT  34359  bj-snsetex  34415  bj-df-v  34487  cover2  35168  releccnveq  35695  rp-fakeinunass  40238  intimag  40372  relexp0eq  40417  ntrneik4w  40818  undif3VD  41603  uzinico  42212  dvnmul  42600  dvnprodlem3  42605  sge00  43030  sge0resplit  43060  sge0fodjrnlem  43070  hspdifhsp  43270  smfresal  43435
 Copyright terms: Public domain W3C validator