Theorem dfcleq 2754

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

Syntax hints:   ↔ wb 208  ∀wal 1557   = wceq 1559   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  cvjust  2755  ax9ALT  2756  eleq2w2  2757  eqriv  2758  eqrdv  2759  eqeq1d  2763  eqeq1dALT  2764  abbib  2830  eqabbw  2834  eleq2d  2847  eleq2dALT  2848  cleqh  2890  nfeqd  2933  cleqf  2951  rexeq  3315  rmoeq1  3397  eqv  3463  abv  3465  csbied  3886  dfss2  3920  eqss  3949  ssequn1  4136  eq0ALT  4301  disj3  4405  undif4  4418  vnexOLD  5265  inex1  5270  axprALT  5376  zfpair2  5388  prex  5392  sucel  6417  uniex2  7716  brtxpsd3  36205  hfext  36494  in-ax8  36545  onsuct0  36762  mh-infprim3bi  36869  eliminable2a  37306  eliminable2b  37307  eliminable2c  37308  eliminable-veqab  37312  eliminable-abeqv  37313  eliminable-abeqab  37314  bj-sbeq  37347  bj-sbceqgALT  37348  bj-snsetex  37409  bj-clex  37477  eleq2w2ALT  37493  wl-cleq-0  37950  wl-cleq-1  37951  wl-cleq-2  37952  wl-cleq-3  37953  wl-cleq-4  37954  wl-cleq-5  37955  wl-cleq-6  37956  cover2  38175  releccnveq  38721  abbibw  43220  rp-fakeinunass  44052  intimag  44193  relexp0eq  44238  ntrneik4w  44637  undif3VD  45418  permaxext  45542  uzinico  46096  dvnmul  46478  dvnprodlem3  46483  sge00  46911  sge0resplit  46941  sge0fodjrnlem  46951  hspdifhsp  47151  smfresal  47323  mo0sn  49398