Theorem dfcleq 2732

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

Syntax hints:   ↔ wb 205  ∀wal 1537   = wceq 1539   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  cvjust  2733  ax9ALT  2734  eleq2w2  2735  eqriv  2736  eqrdv  2737  eqeq1d  2741  eqeq1dALT  2742  abbi  2811  abeq2w  2816  eleq2d  2825  eleq2dALT  2826  cleqh  2863  nfeqd  2918  cleqf  2939  raleqbidvv  3339  eqv  3442  abv  3444  csbied  3871  dfss2  3908  eqss  3937  ssequn1  4115  vn0  4273  eq0  4278  eq0ALT  4279  ab0w  4308  ab0OLD  4310  ab0orv  4313  eq0rdv  4339  disj  4382  disj3  4388  undif4  4401  rzal  4440  ralf0  4445  intprg  4913  vnex  5239  inex1  5242  axprALT  5346  zfpair2  5354  sucel  6343  uniex2  7600  brtxpsd3  34207  hfext  34494  onsuct0  34639  eliminable2a  35053  eliminable2b  35054  eliminable2c  35055  eliminable-veqab  35059  eliminable-abeqv  35060  eliminable-abeqab  35061  bj-sbeq  35095  bj-sbceqgALT  35096  bj-snsetex  35162  eleq2w2ALT  35229  cover2  35881  releccnveq  36405  rp-fakeinunass  41129  intimag  41271  relexp0eq  41316  ntrneik4w  41717  undif3VD  42509  uzinico  43105  dvnmul  43491  dvnprodlem3  43496  sge00  43921  sge0resplit  43951  sge0fodjrnlem  43961  hspdifhsp  44161  smfresal  44333  mo0sn  46172