Theorem dfcleq 2724

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

Syntax hints:   ↔ wb 206  ∀wal 1539   = wceq 1541   ∈ wcel 2111

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 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  cvjust  2725  ax9ALT  2726  eleq2w2  2727  eqriv  2728  eqrdv  2729  eqeq1d  2733  eqeq1dALT  2734  abbib  2800  eqabbw  2804  eleq2d  2817  eleq2dALT  2818  cleqh  2860  nfeqd  2905  cleqf  2923  rexeq  3288  raleqbidvvOLD  3301  rmoeq1  3377  eqv  3446  abv  3448  csbied  3881  dfss2  3915  eqss  3945  ssequn1  4131  vn0  4290  eq0  4295  eq0ALT  4296  ab0w  4324  ab0orv  4328  eq0rdv  4352  disj3  4399  undif4  4412  rzal  4454  ralf0  4459  intprg  4926  vnex  5247  inex1  5250  axprALT  5355  zfpair2  5366  sucel  6377  uniex2  7666  brtxpsd3  35930  hfext  36217  in-ax8  36258  onsuct0  36475  eliminable2a  36894  eliminable2b  36895  eliminable2c  36896  eliminable-veqab  36900  eliminable-abeqv  36901  eliminable-abeqab  36902  bj-sbeq  36935  bj-sbceqgALT  36936  bj-snsetex  36997  bj-clex  37065  eleq2w2ALT  37081  wl-cleq-0  37529  wl-cleq-1  37530  wl-cleq-2  37531  wl-cleq-3  37532  wl-cleq-4  37533  wl-cleq-5  37534  wl-cleq-6  37535  cover2  37755  releccnveq  38293  abbibw  42710  rp-fakeinunass  43548  intimag  43689  relexp0eq  43734  ntrneik4w  44133  undif3VD  44914  permaxext  45038  uzinico  45599  dvnmul  45981  dvnprodlem3  45986  sge00  46414  sge0resplit  46444  sge0fodjrnlem  46454  hspdifhsp  46654  smfresal  46826  mo0sn  48847