Theorem dfcleq 2791

Description: The defining characterization of class equality. It is proved, over Tarski's FOL, from the axiom of (set) extensionality (ax-ext 2771) and the definition of class equality (df-cleq 2790). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2774 to prove also the hypothesis of df-cleq 2790 that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen 1781, equid 2000 }. (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 2774	. 2 ⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧))
2		axextb 2774	. 2 ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))
3	1, 2	df-cleq 2790	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 207  ∀wal 1523   = wceq 1525   ∈ wcel 2083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-cleq 2790

This theorem is referenced by:  cvjust  2792  ax9ALT  2793  eqriv  2794  eqrdv  2795  eqeq1d  2799  eqeq1dALT  2800  eleq2d  2870  eleq2dALT  2871  cleqh  2908  nfeqd  2959  cleqf  2980  eqv  3448  eqss  3910  ssequn1  4083  disj3  4323  undif4  4336  vnex  5116  inex1  5119  axprALT  5221  zfpair2  5229  sucel  6146  uniex2  7329  brtxpsd3  32968  hfext  33255  onsuct0  33400  bj-abbi  33698  eliminable2a  33759  eliminable2b  33760  eliminable2c  33761  bj-ax9  33793  bj-sbeq  33795  bj-sbceqgALT  33796  bj-snsetex  33901  bj-df-v  33966  cover2  34542  releccnveq  35072  rp-fakeinunass  39387  intimag  39507  relexp0eq  39552  ntrneik4w  39956  undif3VD  40776  uzinico  41399  dvnmul  41791  dvnprodlem3  41796  sge00  42222  sge0resplit  42252  sge0fodjrnlem  42262  hspdifhsp  42462  smfresal  42627