Theorem dfcleq 2762

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

Syntax hints:   ↔ wb 209  ∀wal 1565   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  cvjust  2763  ax9ALT  2764  eleq2w2  2765  eqriv  2766  eqrdv  2767  eqeq1d  2771  eqeq1dALT  2772  abbib  2838  eqabbw  2842  eleq2d  2855  eleq2dALT  2856  cleqh  2898  nfeqd  2941  cleqf  2959  rexeq  3325  rmoeq1  3407  eqv  3473  abv  3475  csbied  3897  dfss2  3931  eqss  3960  ssequn1  4147  eq0ALT  4312  disj3  4417  undif4  4430  vnexOLD  5280  inex1  5285  axprALT  5391  zfpair2  5403  prex  5407  sucel  6435  uniex2  7733  brtxpsd3  36281  hfext  36570  in-ax8  36621  onsuct0  36837  mh-infprim3bi  36944  eliminable2a  37380  eliminable2b  37381  eliminable2c  37382  eliminable-veqab  37386  eliminable-abeqv  37387  eliminable-abeqab  37388  bj-sbeq  37421  bj-sbceqgALT  37422  bj-snsetex  37483  bj-clex  37551  eleq2w2ALT  37567  wl-cleq-0  38024  wl-cleq-1  38025  wl-cleq-2  38026  wl-cleq-3  38027  wl-cleq-4  38028  wl-cleq-5  38029  wl-cleq-6  38030  cover2  38249  releccnveq  38795  abbibw  43296  rp-fakeinunass  44128  intimag  44269  relexp0eq  44314  ntrneik4w  44713  undif3VD  45477  permaxext  45601  uzinico  46162  dvnmul  46544  dvnprodlem3  46549  sge00  46977  sge0resplit  47007  sge0fodjrnlem  47017  hspdifhsp  47217  smfresal  47389  mo0sn  49474