Theorem dfcleq 2817

Description: The defining characterization of class equality. It is proved, over Tarski's FOL, from the axiom of (set) extensionality (ax-ext 2795) and the definition of class equality (df-cleq 2816). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2798 to prove also the hypothesis of df-cleq 2816 that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen 1796, 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.

Step	Hyp	Ref	Expression
1		axextb 2798	. 2 ⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧))
2		axextb 2798	. 2 ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))
3	1, 2	df-cleq 2816	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 208  ∀wal 1535   = wceq 1537   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816

This theorem is referenced by:  cvjust  2818  ax9ALT  2819  eqriv  2820  eqrdv  2821  eqeq1d  2825  eqeq1dALT  2826  abbi  2890  eleq2d  2900  eleq2dALT  2901  cleqh  2938  nfeqd  2990  cleqf  3012  eqv  3504  eqss  3984  ssequn1  4158  disj3  4405  undif4  4418  vnex  5220  inex1  5223  axprALT  5325  zfpair2  5333  sucel  6266  uniex2  7466  brtxpsd3  33359  hfext  33646  onsuct0  33791  eliminable2a  34185  eliminable2b  34186  eliminable2c  34187  bj-ax9  34218  bj-sbeq  34220  bj-sbceqgALT  34221  bj-snsetex  34277  bj-df-v  34349  cover2  34991  releccnveq  35521  rp-fakeinunass  39888  intimag  40008  relexp0eq  40053  ntrneik4w  40457  undif3VD  41223  uzinico  41843  dvnmul  42235  dvnprodlem3  42240  sge00  42665  sge0resplit  42695  sge0fodjrnlem  42705  hspdifhsp  42905  smfresal  43070