Theorem dfcleq 2730

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

Syntax hints:   ↔ wb 209  ∀wal 1541   = wceq 1543   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2729

This theorem is referenced by:  cvjust  2731  ax9ALT  2732  eleq2w2  2733  eqriv  2734  eqrdv  2735  eqeq1d  2739  eqeq1dALT  2740  abbi  2810  abeq2w  2815  eleq2d  2823  eleq2dALT  2824  cleqh  2861  nfeqd  2914  cleqf  2935  raleqbidvv  3315  eqv  3417  abv  3419  csbied  3849  dfss2  3886  eqss  3916  ssequn1  4094  vn0  4253  eq0  4258  eq0ALT  4259  ab0w  4288  ab0OLD  4290  ab0orv  4293  eq0rdv  4319  disj  4362  disj3  4368  undif4  4381  rzal  4420  ralf0  4425  intprg  4892  vnex  5207  inex1  5210  axprALT  5315  zfpair2  5323  sucel  6286  uniex2  7526  brtxpsd3  33935  hfext  34222  onsuct0  34367  eliminable2a  34781  eliminable2b  34782  eliminable2c  34783  eliminable-veqab  34787  eliminable-abeqv  34788  eliminable-abeqab  34789  bj-sbeq  34823  bj-sbceqgALT  34824  bj-snsetex  34890  eleq2w2ALT  34957  cover2  35609  releccnveq  36134  rp-fakeinunass  40807  intimag  40941  relexp0eq  40986  ntrneik4w  41387  undif3VD  42175  uzinico  42773  dvnmul  43159  dvnprodlem3  43164  sge00  43589  sge0resplit  43619  sge0fodjrnlem  43629  hspdifhsp  43829  smfresal  43994  mo0sn  45834