Theorem dfcleq 2722

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  cvjust  2723  ax9ALT  2724  eleq2w2  2725  eqriv  2726  eqrdv  2727  eqeq1d  2731  eqeq1dALT  2732  abbib  2798  eqabbw  2802  eleq2d  2814  eleq2dALT  2815  cleqh  2857  nfeqd  2902  cleqf  2920  rexeq  3286  raleqbidvvOLD  3299  rmoeq1  3378  eqv  3448  abv  3450  csbied  3889  dfss2  3923  eqss  3953  ssequn1  4139  vn0  4298  eq0  4303  eq0ALT  4304  ab0w  4332  ab0orv  4336  eq0rdv  4360  disj  4403  disj3  4407  undif4  4420  rzal  4462  ralf0  4467  intprg  4934  vnex  5256  inex1  5259  axprALT  5364  zfpair2  5375  sucel  6387  uniex2  7678  brtxpsd3  35889  hfext  36176  in-ax8  36217  onsuct0  36434  eliminable2a  36853  eliminable2b  36854  eliminable2c  36855  eliminable-veqab  36859  eliminable-abeqv  36860  eliminable-abeqab  36861  bj-sbeq  36894  bj-sbceqgALT  36895  bj-snsetex  36956  bj-clex  37024  eleq2w2ALT  37040  wl-cleq-0  37488  wl-cleq-1  37489  wl-cleq-2  37490  wl-cleq-3  37491  wl-cleq-4  37492  wl-cleq-5  37493  wl-cleq-6  37494  cover2  37714  releccnveq  38252  abbibw  42670  rp-fakeinunass  43508  intimag  43649  relexp0eq  43694  ntrneik4w  44093  undif3VD  44875  permaxext  44999  uzinico  45560  dvnmul  45944  dvnprodlem3  45949  sge00  46377  sge0resplit  46407  sge0fodjrnlem  46417  hspdifhsp  46617  smfresal  46789  mo0sn  48820