Theorem dfcleq 2729

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 2728). Its forward implication is called "class extensionality". Remark: the proof uses axextb 2711 to prove also the hypothesis of df-cleq 2728 that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen 1797, equid 2014 }. (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 2728	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 206  ∀wal 1540   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  cvjust  2730  ax9ALT  2731  eleq2w2  2732  eqriv  2733  eqrdv  2734  eqeq1d  2738  eqeq1dALT  2739  abbib  2805  eqabbw  2809  eleq2d  2822  eleq2dALT  2823  cleqh  2865  nfeqd  2909  cleqf  2927  rexeq  3291  rmoeq1  3373  eqv  3439  abv  3441  csbied  3873  dfss2  3907  eqss  3937  ssequn1  4126  eq0ALT  4291  disj3  4394  undif4  4407  vnexOLD  5253  inex1  5258  axprALT  5364  zfpair2  5376  prex  5380  sucel  6399  uniex2  7692  brtxpsd3  36076  hfext  36365  in-ax8  36406  onsuct0  36623  mh-infprim3bi  36730  eliminable2a  37167  eliminable2b  37168  eliminable2c  37169  eliminable-veqab  37173  eliminable-abeqv  37174  eliminable-abeqab  37175  bj-sbeq  37208  bj-sbceqgALT  37209  bj-snsetex  37270  bj-clex  37338  eleq2w2ALT  37354  wl-cleq-0  37811  wl-cleq-1  37812  wl-cleq-2  37813  wl-cleq-3  37814  wl-cleq-4  37815  wl-cleq-5  37816  wl-cleq-6  37817  cover2  38036  releccnveq  38582  abbibw  43110  rp-fakeinunass  43942  intimag  44083  relexp0eq  44128  ntrneik4w  44527  undif3VD  45308  permaxext  45432  uzinico  45989  dvnmul  46371  dvnprodlem3  46376  sge00  46804  sge0resplit  46834  sge0fodjrnlem  46844  hspdifhsp  47044  smfresal  47216  mo0sn  49291