Theorem dfcleq 2753

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1567   = wceq 1569   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  cvjust  2754  ax9ALT  2755  eleq2w2  2756  eqriv  2757  eqrdv  2758  eqeq1d  2762  eqeq1dALT  2763  abbib  2829  eqabbw  2833  eleq2d  2846  eleq2dALT  2847  cleqh  2889  nfeqd  2932  cleqf  2950  rexeq  3315  rmoeq1  3396  eqv  3460  abv  3462  csbied  3883  eqss  3924  dfss2  4093  ssequn1  4183  eq0ALT  4297  disj3  4406  undif4  4419  vnexOLD  5271  inex1  5276  axprALT  5383  zfpair2  5391  prex  5395  sucel  6441  uniex2  7756  uniex2OLD  7757  brtxpsd3  36752  hfext  37028  in-ax8  37107  onsuct0  37323  mh-infprim3bi  37430  eliminable2a  37866  eliminable2b  37867  eliminable2c  37868  eliminable-veqab  37872  eliminable-abeqv  37873  eliminable-abeqab  37874  bj-sbeq  37907  bj-sbceqgALT  37908  bj-inex1gALT  37931  bj-snsetex  37970  bj-clex  38038  eleq2w2ALT  38068  bj-vn0ALT  38093  wl-cleq-0  38525  wl-cleq-1  38526  wl-cleq-2  38527  wl-cleq-3  38528  wl-cleq-4  38529  wl-cleq-5  38530  wl-cleq-6  38531  cover2  38756  releccnveq  39300  abbibw  43795  rp-fakeinunass  44623  intimag  44763  relexp0eq  44808  ntrneik4w  45207  undif3VD  45971  permaxext  46102  uzinico  46678  dvnmul  47060  dvnprodlem3  47065  sge00  47493  sge0resplit  47523  sge0fodjrnlem  47533  hspdifhsp  47733  smfresal  47905  mo0sn  50034