Theorem dfcleq 2730

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

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

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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  cvjust  2731  ax9ALT  2732  eleq2w2  2733  eqriv  2734  eqrdv  2735  eqeq1d  2739  eqeq1dALT  2740  abbib  2811  eqabbw  2815  eleq2d  2827  eleq2dALT  2828  cleqh  2871  nfeqd  2916  cleqf  2934  rexeq  3322  raleqbidvvOLD  3335  rmoeq1  3416  eqv  3490  abv  3492  csbied  3935  dfss2  3969  eqss  3999  ssequn1  4186  vn0  4345  eq0  4350  eq0ALT  4351  ab0w  4379  ab0orv  4383  eq0rdv  4407  disj  4450  disj3  4454  undif4  4467  rzal  4509  ralf0  4514  intprg  4981  vnex  5314  inex1  5317  axprALT  5422  zfpair2  5433  sucel  6458  uniex2  7758  brtxpsd3  35897  hfext  36184  in-ax8  36225  onsuct0  36442  eliminable2a  36861  eliminable2b  36862  eliminable2c  36863  eliminable-veqab  36867  eliminable-abeqv  36868  eliminable-abeqab  36869  bj-sbeq  36902  bj-sbceqgALT  36903  bj-snsetex  36964  bj-clex  37032  eleq2w2ALT  37048  wl-cleq-0  37496  wl-cleq-1  37497  wl-cleq-2  37498  wl-cleq-3  37499  wl-cleq-4  37500  wl-cleq-5  37501  wl-cleq-6  37502  cover2  37722  releccnveq  38259  abbibw  42687  rp-fakeinunass  43528  intimag  43669  relexp0eq  43714  ntrneik4w  44113  undif3VD  44902  uzinico  45573  dvnmul  45958  dvnprodlem3  45963  sge00  46391  sge0resplit  46421  sge0fodjrnlem  46431  hspdifhsp  46631  smfresal  46803  mo0sn  48735