Theorem dfiun2 5037

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 5034	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
2		dfiun2.1	. . 3 ⊢ 𝐵 ∈ V
3	2	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ V)
4	1, 3	mprg 3068	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   = wceq 1542   ∈ wcel 2107  {cab 2710  ∃wrex 3071  Vcvv 3475  ∪ cuni 4909  ∪ ciun 4998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-11 2155  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-v 3477  df-uni 4910  df-iun 5000

This theorem is referenced by:  fniunfv  7246  funcnvuni  7922  fiun  7929  f1iun  7930  tfrlem8  8384  rdglim2a  8433  rankuni  9858  cardiun  9977  kmlem11  10155  cfslb2n  10263  enfin2i  10316  pwcfsdom  10578  rankcf  10772  tskuni  10778  discmp  22902  cmpsublem  22903  cmpsub  22904  nnoeomeqom  42062