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  3292  raleqbidvvOLD  3305  rmoeq1  3384  eqv  3454  abv  3456  csbied  3895  dfss2  3929  eqss  3959  ssequn1  4145  vn0  4304  eq0  4309  eq0ALT  4310  ab0w  4338  ab0orv  4342  eq0rdv  4366  disj  4409  disj3  4413  undif4  4426  rzal  4468  ralf0  4473  intprg  4941  vnex  5264  inex1  5267  axprALT  5372  zfpair2  5383  sucel  6396  uniex2  7694  brtxpsd3  35857  hfext  36144  in-ax8  36185  onsuct0  36402  eliminable2a  36821  eliminable2b  36822  eliminable2c  36823  eliminable-veqab  36827  eliminable-abeqv  36828  eliminable-abeqab  36829  bj-sbeq  36862  bj-sbceqgALT  36863  bj-snsetex  36924  bj-clex  36992  eleq2w2ALT  37008  wl-cleq-0  37456  wl-cleq-1  37457  wl-cleq-2  37458  wl-cleq-3  37459  wl-cleq-4  37460  wl-cleq-5  37461  wl-cleq-6  37462  cover2  37682  releccnveq  38220  abbibw  42638  rp-fakeinunass  43477  intimag  43618  relexp0eq  43663  ntrneik4w  44062  undif3VD  44844  permaxext  44968  uzinico  45530  dvnmul  45914  dvnprodlem3  45919  sge00  46347  sge0resplit  46377  sge0fodjrnlem  46387  hspdifhsp  46587  smfresal  46759  mo0sn  48777