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 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 2735	. 2 ⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧))
2		axextb 2735	. 2 ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))
3	1, 2	df-cleq 2752	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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  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  dfss2  3917  eqss  3946  ssequn1  4132  eq0ALT  4298  disj3  4407  undif4  4420  vnexOLD  5275  inex1  5280  axprALT  5387  zfpair2  5399  prex  5403  sucel  6434  uniex2  7739  uniex2OLD  7740  brtxpsd3  36473  hfext  36763  in-ax8  36844  onsuct0  37060  mh-infprim3bi  37167  eliminable2a  37603  eliminable2b  37604  eliminable2c  37605  eliminable-veqab  37609  eliminable-abeqv  37610  eliminable-abeqab  37611  bj-sbeq  37644  bj-sbceqgALT  37645  bj-inex1gALT  37668  bj-snsetex  37707  bj-clex  37775  eleq2w2ALT  37791  bj-vn0ALT  37816  wl-cleq-0  38249  wl-cleq-1  38250  wl-cleq-2  38251  wl-cleq-3  38252  wl-cleq-4  38253  wl-cleq-5  38254  wl-cleq-6  38255  cover2  38465  releccnveq  39009  abbibw  43523  rp-fakeinunass  44355  intimag  44496  relexp0eq  44541  ntrneik4w  44940  undif3VD  45704  permaxext  45828  uzinico  46389  dvnmul  46771  dvnprodlem3  46776  sge00  47204  sge0resplit  47234  sge0fodjrnlem  47244  hspdifhsp  47444  smfresal  47616  mo0sn  49744