Theorem dfcleq 2732

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 2731). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2714 to prove also the hypothesis of df-cleq 2731 that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen 1802, equid 2019 }. (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 2731	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 207  ∀wal 1545   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  cvjust  2733  ax9ALT  2734  eleq2w2  2735  eqriv  2736  eqrdv  2737  eqeq1d  2741  eqeq1dALT  2742  abbib  2808  eqabbw  2812  eleq2d  2825  eleq2dALT  2826  cleqh  2868  nfeqd  2911  cleqf  2929  rexeq  3293  rmoeq1  3375  eqv  3441  abv  3443  csbied  3867  dfss2  3901  eqss  3930  ssequn1  4115  eq0ALT  4279  disj3  4382  undif4  4395  vnexOLD  5240  inex1  5245  axprALT  5351  zfpair2  5363  prex  5367  sucel  6386  uniex2  7681  brtxpsd3  36122  hfext  36411  in-ax8  36452  onsuct0  36669  mh-infprim3bi  36776  eliminable2a  37213  eliminable2b  37214  eliminable2c  37215  eliminable-veqab  37219  eliminable-abeqv  37220  eliminable-abeqab  37221  bj-sbeq  37254  bj-sbceqgALT  37255  bj-snsetex  37316  bj-clex  37384  eleq2w2ALT  37400  wl-cleq-0  37857  wl-cleq-1  37858  wl-cleq-2  37859  wl-cleq-3  37860  wl-cleq-4  37861  wl-cleq-5  37862  wl-cleq-6  37863  cover2  38082  releccnveq  38628  abbibw  43127  rp-fakeinunass  43959  intimag  44100  relexp0eq  44145  ntrneik4w  44544  undif3VD  45325  permaxext  45449  uzinico  46004  dvnmul  46386  dvnprodlem3  46391  sge00  46819  sge0resplit  46849  sge0fodjrnlem  46859  hspdifhsp  47059  smfresal  47231  mo0sn  49306