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  3931  dfss2  3968  eqss  3997  ssequn1  4180  vn0  4338  eq0  4343  eq0ALT  4344  ab0w  4373  ab0OLD  4375  ab0orv  4378  eq0rdv  4404  disj  4447  disj3  4453  undif4  4466  rzal  4508  ralf0  4513  intprg  4985  vnex  5314  inex1  5317  axprALT  5420  zfpair2  5428  sucel  6436  uniex2  7725  brtxpsd3  34857  hfext  35144  onsuct0  35315  eliminable2a  35728  eliminable2b  35729  eliminable2c  35730  eliminable-veqab  35734  eliminable-abeqv  35735  eliminable-abeqab  35736  bj-sbeq  35770  bj-sbceqgALT  35771  bj-snsetex  35833  bj-clex  35901  eleq2w2ALT  35917  cover2  36572  releccnveq  37115  rp-fakeinunass  42252  intimag  42393  relexp0eq  42438  ntrneik4w  42837  undif3VD  43629  uzinico  44260  dvnmul  44646  dvnprodlem3  44651  sge00  45079  sge0resplit  45109  sge0fodjrnlem  45119  hspdifhsp  45319  smfresal  45491  mo0sn  47454