Theorem dfcleq 2731

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  cvjust  2732  ax9ALT  2733  eleq2w2  2734  eqriv  2735  eqrdv  2736  eqeq1d  2740  eqeq1dALT  2741  abbi  2811  abeq2w  2816  eleq2d  2824  eleq2dALT  2825  cleqh  2862  nfeqd  2916  cleqf  2937  raleqbidvv  3329  eqv  3431  abv  3433  csbied  3866  dfss2  3903  eqss  3932  ssequn1  4110  vn0  4269  eq0  4274  eq0ALT  4275  ab0w  4304  ab0OLD  4306  ab0orv  4309  eq0rdv  4335  disj  4378  disj3  4384  undif4  4397  rzal  4436  ralf0  4441  intprg  4909  vnex  5233  inex1  5236  axprALT  5340  zfpair2  5348  sucel  6324  uniex2  7569  brtxpsd3  34125  hfext  34412  onsuct0  34557  eliminable2a  34971  eliminable2b  34972  eliminable2c  34973  eliminable-veqab  34977  eliminable-abeqv  34978  eliminable-abeqab  34979  bj-sbeq  35013  bj-sbceqgALT  35014  bj-snsetex  35080  eleq2w2ALT  35147  cover2  35799  releccnveq  36324  rp-fakeinunass  41020  intimag  41153  relexp0eq  41198  ntrneik4w  41599  undif3VD  42391  uzinico  42988  dvnmul  43374  dvnprodlem3  43379  sge00  43804  sge0resplit  43834  sge0fodjrnlem  43844  hspdifhsp  44044  smfresal  44209  mo0sn  46049