Theorem dfcleq 2758

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

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

This theorem is used by:  cvjust  2759  ax9ALT  2760  eleq2w2  2761  eqriv  2762  eqrdv  2763  eqeq1d  2767  eqeq1dALT  2768  abbib  2834  eqabbw  2838  eleq2d  2851  eleq2dALT  2852  cleqh  2894  nfeqd  2937  cleqf  2955  rexeq  3321  rmoeq1  3402  eqv  3467  abv  3469  csbied  3890  dfss2  3924  eqss  3953  ssequn1  4139  eq0ALT  4305  disj3  4414  undif4  4427  vnexOLD  5283  inex1  5288  axprALT  5395  zfpair2  5407  prex  5411  sucel  6441  uniex2  7741  uniex2OLD  7742  brtxpsd3  36399  hfext  36688  in-ax8  36769  onsuct0  36985  mh-infprim3bi  37092  eliminable2a  37528  eliminable2b  37529  eliminable2c  37530  eliminable-veqab  37534  eliminable-abeqv  37535  eliminable-abeqab  37536  bj-sbeq  37569  bj-sbceqgALT  37570  bj-inex1gALT  37593  bj-snsetex  37632  bj-clex  37700  eleq2w2ALT  37716  bj-vn0ALT  37741  wl-cleq-0  38174  wl-cleq-1  38175  wl-cleq-2  38176  wl-cleq-3  38177  wl-cleq-4  38178  wl-cleq-5  38179  wl-cleq-6  38180  cover2  38399  releccnveq  38943  abbibw  43442  rp-fakeinunass  44274  intimag  44415  relexp0eq  44460  ntrneik4w  44859  undif3VD  45623  permaxext  45747  uzinico  46308  dvnmul  46690  dvnprodlem3  46695  sge00  47123  sge0resplit  47153  sge0fodjrnlem  47163  hspdifhsp  47363  smfresal  47535  mo0sn  49627