Theorem dfiun2 4991

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

Syntax hints:   = wceq 1562   ∈ wcel 2144  {cab 2742  ∃wrex 3088  Vcvv 3456  ∪ cuni 4867  ∪ ciun 4951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-11 2193  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-v 3458  df-uni 4868  df-iun 4953

This theorem is referenced by:  fniunfv  7233  funcnvuni  7915  fiun  7926  f1iun  7927  tfrlem8  8357  rdglim2a  8406  rankuni  9823  cardiun  9942  kmlem11  10119  cfslb2n  10227  enfin2i  10280  pwcfsdom  10543  rankcf  10737  tskuni  10743  discmp  23460  cmpsublem  23461  cmpsub  23462  rankfilimbi  35401  nmulprop  36545  nnoeomeqom  43894