Theorem dfcleq 2756

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1568   = wceq 1570   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  cvjust  2757  ax9ALT  2758  eleq2w2  2759  eqriv  2760  eqrdv  2761  eqeq1d  2765  eqeq1dALT  2766  abbib  2832  abbibOLD  2833  eqabbw  2837  eleq2d  2850  eleq2dALT  2851  cleqh  2893  nfeqd  2936  cleqf  2954  rexeq  3319  rmoeq1  3400  eqv  3464  abv  3466  csbied  3887  eqss  3928  dfss2  4097  ssequn1  4187  eq0ALT  4301  disj3  4410  undif4  4423  vnexOLD  5278  inex1  5284  axprALT  5391  zfpair2  5399  prex  5403  sucel  6465  uniex2  7786  uniex2OLD  7787  brtxpsd3  36873  hfext  37149  in-ax8  37228  onsuct0  37444  mh-infprim3bi  37551  eliminable2a  37987  eliminable2b  37988  eliminable2c  37989  eliminable-veqab  37993  eliminable-abeqv  37994  eliminable-abeqab  37995  bj-sbeq  38028  bj-sbceqgALT  38029  bj-inex1gALT  38052  bj-snsetex  38091  bj-clex  38159  eleq2w2ALT  38232  bj-vn0ALT  38257  wl-cleq-0  38686  wl-cleq-1  38687  wl-cleq-2  38688  wl-cleq-3  38689  wl-cleq-4  38690  wl-cleq-5  38691  wl-cleq-6  38692  cover2  38917  releccnveq  39459  abbibw  43954  rp-fakeinunass  44777  intimag  44917  relexp0eq  44962  ntrneik4w  45361  undif3VD  46124  permaxext  46259  uzinico  46844  dvnmul  47226  dvnprodlem3  47231  sge00  47659  sge0resplit  47689  sge0fodjrnlem  47699  hspdifhsp  47899  smfresal  48071  mo0sn  50258