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 1796, equid 2013 }. (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 1539   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  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  3292  raleqbidvvOLD  3305  rmoeq1  3381  eqv  3450  abv  3452  csbied  3885  dfss2  3919  eqss  3949  ssequn1  4138  eq0ALT  4303  disj3  4406  undif4  4419  intprg  4936  vnex  5259  inex1  5262  axprALT  5367  zfpair2  5378  sucel  6393  uniex2  7683  brtxpsd3  36088  hfext  36377  in-ax8  36418  onsuct0  36635  eliminable2a  37061  eliminable2b  37062  eliminable2c  37063  eliminable-veqab  37067  eliminable-abeqv  37068  eliminable-abeqab  37069  bj-sbeq  37102  bj-sbceqgALT  37103  bj-snsetex  37164  bj-clex  37232  eleq2w2ALT  37248  wl-cleq-0  37700  wl-cleq-1  37701  wl-cleq-2  37702  wl-cleq-3  37703  wl-cleq-4  37704  wl-cleq-5  37705  wl-cleq-6  37706  cover2  37916  releccnveq  38456  abbibw  42920  rp-fakeinunass  43756  intimag  43897  relexp0eq  43942  ntrneik4w  44341  undif3VD  45122  permaxext  45246  uzinico  45805  dvnmul  46187  dvnprodlem3  46192  sge00  46620  sge0resplit  46650  sge0fodjrnlem  46660  hspdifhsp  46860  smfresal  47032  mo0sn  49061