Theorem dfcleq 2728

Description: The defining characterization of class equality. It is proved, over Tarski's FOL, from the axiom of (set) extensionality (ax-ext 2707) and the definition of class equality (df-cleq 2727). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2710 to prove also the hypothesis of df-cleq 2727 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 2710	. 2 ⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧))
2		axextb 2710	. 2 ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))
3	1, 2	df-cleq 2727	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 2707

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

This theorem is referenced by:  cvjust  2729  ax9ALT  2730  eleq2w2  2731  eqriv  2732  eqrdv  2733  eqeq1d  2737  eqeq1dALT  2738  abbib  2804  eqabbw  2808  eleq2d  2820  eleq2dALT  2821  cleqh  2864  nfeqd  2909  cleqf  2927  rexeq  3301  raleqbidvvOLD  3314  rmoeq1  3395  eqv  3469  abv  3471  csbied  3910  dfss2  3944  eqss  3974  ssequn1  4161  vn0  4320  eq0  4325  eq0ALT  4326  ab0w  4354  ab0orv  4358  eq0rdv  4382  disj  4425  disj3  4429  undif4  4442  rzal  4484  ralf0  4489  intprg  4957  vnex  5284  inex1  5287  axprALT  5392  zfpair2  5403  sucel  6428  uniex2  7732  brtxpsd3  35914  hfext  36201  in-ax8  36242  onsuct0  36459  eliminable2a  36878  eliminable2b  36879  eliminable2c  36880  eliminable-veqab  36884  eliminable-abeqv  36885  eliminable-abeqab  36886  bj-sbeq  36919  bj-sbceqgALT  36920  bj-snsetex  36981  bj-clex  37049  eleq2w2ALT  37065  wl-cleq-0  37513  wl-cleq-1  37514  wl-cleq-2  37515  wl-cleq-3  37516  wl-cleq-4  37517  wl-cleq-5  37518  wl-cleq-6  37519  cover2  37739  releccnveq  38276  abbibw  42700  rp-fakeinunass  43539  intimag  43680  relexp0eq  43725  ntrneik4w  44124  undif3VD  44906  permaxext  45030  uzinico  45588  dvnmul  45972  dvnprodlem3  45977  sge00  46405  sge0resplit  46435  sge0fodjrnlem  46445  hspdifhsp  46645  smfresal  46817  mo0sn  48794