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 2709) and the definition of class equality (df-cleq 2729). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2712 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 1797, equid 2014 }. (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 2729	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 206  ∀wal 1540   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  cvjust  2731  ax9ALT  2732  eleq2w2  2733  eqriv  2734  eqrdv  2735  eqeq1d  2739  eqeq1dALT  2740  abbib  2806  eqabbw  2810  eleq2d  2823  eleq2dALT  2824  cleqh  2866  nfeqd  2910  cleqf  2928  rexeq  3292  rmoeq1  3374  eqv  3440  abv  3442  csbied  3874  dfss2  3908  eqss  3938  ssequn1  4127  eq0ALT  4292  disj3  4395  undif4  4408  vnex  5251  inex1  5254  axprALT  5359  zfpair2  5371  prex  5375  sucel  6393  uniex2  7685  brtxpsd3  36092  hfext  36381  in-ax8  36422  onsuct0  36639  mh-infprim3bi  36746  eliminable2a  37183  eliminable2b  37184  eliminable2c  37185  eliminable-veqab  37189  eliminable-abeqv  37190  eliminable-abeqab  37191  bj-sbeq  37224  bj-sbceqgALT  37225  bj-snsetex  37286  bj-clex  37354  eleq2w2ALT  37370  wl-cleq-0  37825  wl-cleq-1  37826  wl-cleq-2  37827  wl-cleq-3  37828  wl-cleq-4  37829  wl-cleq-5  37830  wl-cleq-6  37831  cover2  38050  releccnveq  38596  abbibw  43124  rp-fakeinunass  43960  intimag  44101  relexp0eq  44146  ntrneik4w  44545  undif3VD  45326  permaxext  45450  uzinico  46007  dvnmul  46389  dvnprodlem3  46394  sge00  46822  sge0resplit  46852  sge0fodjrnlem  46862  hspdifhsp  47062  smfresal  47234  mo0sn  49303