Theorem dfcleq 2733

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

Syntax hints:   ↔ wb 206  ∀wal 1535   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  cvjust  2734  ax9ALT  2735  eleq2w2  2736  eqriv  2737  eqrdv  2738  eqeq1d  2742  eqeq1dALT  2743  abbib  2814  eqabbw  2818  eleq2d  2830  eleq2dALT  2831  cleqh  2874  nfeqd  2919  cleqf  2940  rexeq  3330  raleqbidvvOLD  3343  rmoeq1  3425  eqv  3498  abv  3500  csbied  3959  dfss2  3994  eqss  4024  ssequn1  4209  vn0  4368  eq0  4373  eq0ALT  4374  ab0w  4401  ab0OLD  4403  ab0orv  4406  eq0rdv  4430  disj  4473  disj3  4477  undif4  4490  rzal  4532  ralf0  4537  intprg  5005  vnex  5332  inex1  5335  axprALT  5440  zfpair2  5448  sucel  6469  uniex2  7773  brtxpsd3  35860  hfext  36147  in-ax8  36190  onsuct0  36407  eliminable2a  36826  eliminable2b  36827  eliminable2c  36828  eliminable-veqab  36832  eliminable-abeqv  36833  eliminable-abeqab  36834  bj-sbeq  36867  bj-sbceqgALT  36868  bj-snsetex  36929  bj-clex  36997  eleq2w2ALT  37013  cover2  37675  releccnveq  38214  abbibw  42632  rp-fakeinunass  43477  intimag  43618  relexp0eq  43663  ntrneik4w  44062  undif3VD  44853  uzinico  45478  dvnmul  45864  dvnprodlem3  45869  sge00  46297  sge0resplit  46327  sge0fodjrnlem  46337  hspdifhsp  46537  smfresal  46709  mo0sn  48547