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 2706) and the definition of class equality (df-cleq 2727). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2709 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 1792, equid 2009 }. (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 2709	. 2 ⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧))
2		axextb 2709	. 2 ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))
3	1, 2	df-cleq 2727	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 206  ∀wal 1535   = wceq 1537   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

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

This theorem is referenced by:  cvjust  2729  ax9ALT  2730  eleq2w2  2731  eqriv  2732  eqrdv  2733  eqeq1d  2737  eqeq1dALT  2738  abbib  2809  eqabbw  2813  eleq2d  2825  eleq2dALT  2826  cleqh  2869  nfeqd  2914  cleqf  2932  rexeq  3320  raleqbidvvOLD  3333  rmoeq1  3414  eqv  3488  abv  3490  csbied  3946  dfss2  3981  eqss  4011  ssequn1  4196  vn0  4351  eq0  4356  eq0ALT  4357  ab0w  4385  ab0orv  4389  eq0rdv  4413  disj  4456  disj3  4460  undif4  4473  rzal  4515  ralf0  4520  intprg  4986  vnex  5320  inex1  5323  axprALT  5428  zfpair2  5439  sucel  6460  uniex2  7757  brtxpsd3  35878  hfext  36165  in-ax8  36207  onsuct0  36424  eliminable2a  36843  eliminable2b  36844  eliminable2c  36845  eliminable-veqab  36849  eliminable-abeqv  36850  eliminable-abeqab  36851  bj-sbeq  36884  bj-sbceqgALT  36885  bj-snsetex  36946  bj-clex  37014  eleq2w2ALT  37030  wl-cleq-0  37478  wl-cleq-1  37479  wl-cleq-2  37480  wl-cleq-3  37481  wl-cleq-4  37482  cover2  37702  releccnveq  38240  abbibw  42664  rp-fakeinunass  43505  intimag  43646  relexp0eq  43691  ntrneik4w  44090  undif3VD  44880  uzinico  45513  dvnmul  45899  dvnprodlem3  45904  sge00  46332  sge0resplit  46362  sge0fodjrnlem  46372  hspdifhsp  46572  smfresal  46744  mo0sn  48664