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 1825, equid 2042 }. (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 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 209  ∀wal 1568   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  cvjust  2757  ax9ALT  2758  eleq2w2  2759  eqriv  2760  eqrdv  2761  eqeq1d  2765  eqeq1dALT  2766  abbib  2832  eqabbw  2836  eleq2d  2849  eleq2dALT  2850  cleqh  2892  nfeqd  2935  cleqf  2953  rexeq  3319  rmoeq1  3400  eqv  3465  abv  3467  csbied  3889  dfss2  3923  eqss  3952  ssequn1  4139  eq0ALT  4305  disj3  4414  undif4  4427  vnexOLD  5281  inex1  5286  axprALT  5393  zfpair2  5405  prex  5409  sucel  6437  uniex2  7735  uniex2OLD  7736  brtxpsd3  36386  hfext  36675  in-ax8  36736  onsuct0  36952  mh-infprim3bi  37059  eliminable2a  37495  eliminable2b  37496  eliminable2c  37497  eliminable-veqab  37501  eliminable-abeqv  37502  eliminable-abeqab  37503  bj-sbeq  37536  bj-sbceqgALT  37537  bj-inex1gALT  37560  bj-snsetex  37599  bj-clex  37667  eleq2w2ALT  37683  bj-vn0ALT  37708  wl-cleq-0  38141  wl-cleq-1  38142  wl-cleq-2  38143  wl-cleq-3  38144  wl-cleq-4  38145  wl-cleq-5  38146  wl-cleq-6  38147  cover2  38366  releccnveq  38910  abbibw  43409  rp-fakeinunass  44241  intimag  44382  relexp0eq  44427  ntrneik4w  44826  undif3VD  45590  permaxext  45714  uzinico  46275  dvnmul  46657  dvnprodlem3  46662  sge00  47090  sge0resplit  47120  sge0fodjrnlem  47130  hspdifhsp  47330  smfresal  47502  mo0sn  49594