Theorem dfcleq 2726

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

Syntax hints:   ↔ wb 205  ∀wal 1540   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  cvjust  2727  ax9ALT  2728  eleq2w2  2729  eqriv  2730  eqrdv  2731  eqeq1d  2735  eqeq1dALT  2736  abbib  2805  eqabbw  2810  eleq2d  2820  eleq2dALT  2821  cleqh  2864  nfeqd  2914  cleqf  2935  rexeq  3322  raleqbidvvOLD  3331  raleleq  3338  rmoeq1  3415  eqv  3484  abv  3486  csbied  3932  dfss2  3969  eqss  3998  ssequn1  4181  vn0  4339  eq0  4344  eq0ALT  4345  ab0w  4374  ab0OLD  4376  ab0orv  4379  eq0rdv  4405  disj  4448  disj3  4454  undif4  4467  rzal  4509  ralf0  4514  intprg  4986  vnex  5315  inex1  5318  axprALT  5421  zfpair2  5429  sucel  6439  uniex2  7728  brtxpsd3  34899  hfext  35186  onsuct0  35374  eliminable2a  35787  eliminable2b  35788  eliminable2c  35789  eliminable-veqab  35793  eliminable-abeqv  35794  eliminable-abeqab  35795  bj-sbeq  35829  bj-sbceqgALT  35830  bj-snsetex  35892  bj-clex  35960  eleq2w2ALT  35976  cover2  36631  releccnveq  37174  rp-fakeinunass  42314  intimag  42455  relexp0eq  42500  ntrneik4w  42899  undif3VD  43691  uzinico  44321  dvnmul  44707  dvnprodlem3  44712  sge00  45140  sge0resplit  45170  sge0fodjrnlem  45180  hspdifhsp  45380  smfresal  45552  mo0sn  47548