Theorem dfcleq 2722

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

Syntax hints:   ↔ wb 206  ∀wal 1538   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  cvjust  2723  ax9ALT  2724  eleq2w2  2725  eqriv  2726  eqrdv  2727  eqeq1d  2731  eqeq1dALT  2732  abbib  2798  eqabbw  2802  eleq2d  2814  eleq2dALT  2815  cleqh  2857  nfeqd  2902  cleqf  2920  rexeq  3295  raleqbidvvOLD  3308  rmoeq1  3387  eqv  3457  abv  3459  csbied  3898  dfss2  3932  eqss  3962  ssequn1  4149  vn0  4308  eq0  4313  eq0ALT  4314  ab0w  4342  ab0orv  4346  eq0rdv  4370  disj  4413  disj3  4417  undif4  4430  rzal  4472  ralf0  4477  intprg  4945  vnex  5269  inex1  5272  axprALT  5377  zfpair2  5388  sucel  6408  uniex2  7714  brtxpsd3  35884  hfext  36171  in-ax8  36212  onsuct0  36429  eliminable2a  36848  eliminable2b  36849  eliminable2c  36850  eliminable-veqab  36854  eliminable-abeqv  36855  eliminable-abeqab  36856  bj-sbeq  36889  bj-sbceqgALT  36890  bj-snsetex  36951  bj-clex  37019  eleq2w2ALT  37035  wl-cleq-0  37483  wl-cleq-1  37484  wl-cleq-2  37485  wl-cleq-3  37486  wl-cleq-4  37487  wl-cleq-5  37488  wl-cleq-6  37489  cover2  37709  releccnveq  38247  abbibw  42665  rp-fakeinunass  43504  intimag  43645  relexp0eq  43690  ntrneik4w  44089  undif3VD  44871  permaxext  44995  uzinico  45557  dvnmul  45941  dvnprodlem3  45946  sge00  46374  sge0resplit  46404  sge0fodjrnlem  46414  hspdifhsp  46614  smfresal  46786  mo0sn  48804