Theorem dfiun2 4989

Description: Alternate definition of indexed union when 𝐵 is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 27-Jun-1998.) (Revised by David Abernethy, 19-Jun-2012.)

Hypothesis

Ref	Expression
dfiun2.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
dfiun2	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝑦,𝐵

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem dfiun2

Step	Hyp	Ref	Expression
1		dfiun2g 4987	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
2		dfiun2.1	. . 3 ⊢ 𝐵 ∈ V
3	2	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ V)
4	1, 3	mprg 3082	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  {cab 2738  ∃wrex 3086  Vcvv 3450  ∪ cuni 4866  ∪ ciun 4950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-11 2193  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-uni 4867  df-iun 4952

This theorem is used by:  fniunfv  7251  funcnvuni  7944  fiun  7955  f1iun  7956  tfrlem8  8392  rdglim2a  8441  rankuni  9879  rankfilimbi  9902  cardiun  10063  kmlem11  10239  cfslb2n  10346  enfin2i  10399  pwcfsdom  10668  rankcf  10862  tskuni  10868  discmp  23716  cmpsublem  23717  cmpsub  23718  nmulprop  36939  nnoeomeqom  44314