Theorem dfcleq 2723

Description: The defining characterization of class equality. It is proved, over Tarski's FOL, from the axiom of (set) extensionality (ax-ext 2702) and the definition of class equality (df-cleq 2722). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2705 to prove also the hypothesis of df-cleq 2722 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 2705	. 2 ⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧))
2		axextb 2705	. 2 ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))
3	1, 2	df-cleq 2722	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 2702

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

This theorem is referenced by:  cvjust  2724  ax9ALT  2725  eleq2w2  2726  eqriv  2727  eqrdv  2728  eqeq1d  2732  eqeq1dALT  2733  abbib  2799  eqabbw  2803  eleq2d  2815  eleq2dALT  2816  cleqh  2858  nfeqd  2903  cleqf  2921  rexeq  3297  raleqbidvvOLD  3310  rmoeq1  3390  eqv  3460  abv  3462  csbied  3901  dfss2  3935  eqss  3965  ssequn1  4152  vn0  4311  eq0  4316  eq0ALT  4317  ab0w  4345  ab0orv  4349  eq0rdv  4373  disj  4416  disj3  4420  undif4  4433  rzal  4475  ralf0  4480  intprg  4948  vnex  5272  inex1  5275  axprALT  5380  zfpair2  5391  sucel  6411  uniex2  7717  brtxpsd3  35891  hfext  36178  in-ax8  36219  onsuct0  36436  eliminable2a  36855  eliminable2b  36856  eliminable2c  36857  eliminable-veqab  36861  eliminable-abeqv  36862  eliminable-abeqab  36863  bj-sbeq  36896  bj-sbceqgALT  36897  bj-snsetex  36958  bj-clex  37026  eleq2w2ALT  37042  wl-cleq-0  37490  wl-cleq-1  37491  wl-cleq-2  37492  wl-cleq-3  37493  wl-cleq-4  37494  wl-cleq-5  37495  wl-cleq-6  37496  cover2  37716  releccnveq  38254  abbibw  42672  rp-fakeinunass  43511  intimag  43652  relexp0eq  43697  ntrneik4w  44096  undif3VD  44878  permaxext  45002  uzinico  45564  dvnmul  45948  dvnprodlem3  45953  sge00  46381  sge0resplit  46411  sge0fodjrnlem  46421  hspdifhsp  46621  smfresal  46793  mo0sn  48808