Theorem dfcleq 2722

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

Syntax hints:   ↔ wb 206  ∀wal 1538   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  cvjust  2723  ax9ALT  2724  eleq2w2  2725  eqriv  2726  eqrdv  2727  eqeq1d  2731  eqeq1dALT  2732  abbib  2798  eqabbw  2802  eleq2d  2814  eleq2dALT  2815  cleqh  2857  nfeqd  2902  cleqf  2920  rexeq  3285  raleqbidvvOLD  3298  rmoeq1  3376  eqv  3446  abv  3448  csbied  3887  dfss2  3921  eqss  3951  ssequn1  4137  vn0  4296  eq0  4301  eq0ALT  4302  ab0w  4330  ab0orv  4334  eq0rdv  4358  disj  4401  disj3  4405  undif4  4418  rzal  4460  ralf0  4465  intprg  4931  vnex  5253  inex1  5256  axprALT  5361  zfpair2  5372  sucel  6383  uniex2  7674  brtxpsd3  35890  hfext  36177  in-ax8  36218  onsuct0  36435  eliminable2a  36854  eliminable2b  36855  eliminable2c  36856  eliminable-veqab  36860  eliminable-abeqv  36861  eliminable-abeqab  36862  bj-sbeq  36895  bj-sbceqgALT  36896  bj-snsetex  36957  bj-clex  37025  eleq2w2ALT  37041  wl-cleq-0  37489  wl-cleq-1  37490  wl-cleq-2  37491  wl-cleq-3  37492  wl-cleq-4  37493  wl-cleq-5  37494  wl-cleq-6  37495  cover2  37715  releccnveq  38253  abbibw  42670  rp-fakeinunass  43508  intimag  43649  relexp0eq  43694  ntrneik4w  44093  undif3VD  44875  permaxext  44999  uzinico  45560  dvnmul  45944  dvnprodlem3  45949  sge00  46377  sge0resplit  46407  sge0fodjrnlem  46417  hspdifhsp  46617  smfresal  46789  mo0sn  48820