Theorem dfcleq 2754

Description: The defining characterization of class equality. It is proved, over Tarski's FOL, from the axiom of (set) extensionality (ax-ext 2733) and the definition of class equality (df-cleq 2753). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2736 to prove also the hypothesis of df-cleq 2753 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 2736	. 2 ⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧))
2		axextb 2736	. 2 ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))
3	1, 2	df-cleq 2753	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

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

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 2155  ax-ext 2733

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

This theorem is used by:  cvjust  2755  ax9ALT  2756  eleq2w2  2757  eqriv  2758  eqrdv  2759  eqeq1d  2763  eqeq1dALT  2764  abbib  2830  eqabbw  2834  eleq2d  2847  eleq2dALT  2848  cleqh  2890  nfeqd  2933  cleqf  2951  rexeq  3316  rmoeq1  3397  eqv  3461  abv  3463  csbied  3883  dfss2  3917  eqss  3946  ssequn1  4132  eq0ALT  4298  disj3  4407  undif4  4420  vnexOLD  5272  inex1  5277  axprALT  5384  zfpair2  5392  prex  5396  sucel  6438  uniex2  7752  uniex2OLD  7753  brtxpsd3  36638  hfext  36914  in-ax8  36993  onsuct0  37209  mh-infprim3bi  37316  eliminable2a  37752  eliminable2b  37753  eliminable2c  37754  eliminable-veqab  37758  eliminable-abeqv  37759  eliminable-abeqab  37760  bj-sbeq  37793  bj-sbceqgALT  37794  bj-inex1gALT  37817  bj-snsetex  37856  bj-clex  37924  eleq2w2ALT  37942  bj-vn0ALT  37967  wl-cleq-0  38398  wl-cleq-1  38399  wl-cleq-2  38400  wl-cleq-3  38401  wl-cleq-4  38402  wl-cleq-5  38403  wl-cleq-6  38404  cover2  38629  releccnveq  39173  abbibw  43668  rp-fakeinunass  44500  intimag  44641  relexp0eq  44686  ntrneik4w  45085  undif3VD  45849  permaxext  45973  uzinico  46540  dvnmul  46922  dvnprodlem3  46927  sge00  47355  sge0resplit  47385  sge0fodjrnlem  47395  hspdifhsp  47595  smfresal  47767  mo0sn  49895