Theorem dfiun3g 5947

Description: Alternate definition of indexed union when 𝐵 is a set. (Contributed by Mario Carneiro, 31-Aug-2015.)

Assertion

Ref	Expression
dfiun3g	⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵))

Proof of Theorem dfiun3g

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfiun2g 4988	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
2		eqid 2760	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	rnmpt 5936	. . 3 ⊢ ran (𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
4	3	unieqi 4879	. 2 ⊢ ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
5	1, 4	eqtr4di 2813	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran (𝑥 ∈ 𝐴 ↦ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {cab 2738  ∀wral 3076  ∃wrex 3086  ∪ cuni 4867  ∪ ciun 4951   ↦ cmpt 5186  ran crn 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-cnv 5656  df-dm 5658  df-rn 5659

This theorem is used by:  dfiun3  5949  iunon  8326  onoviun  8330  gruiun  10841  tgiun  23244  acunirnmpt2f  33174  locfinreflem  34391  carsgclctunlem2  34871  pmeasadd  34877  saliunclf  47248  salexct3  47268  salgensscntex  47270  meadjiun  47392  omeiunle  47443  ovolval5lem2  47579  tmachlem-uassst  47869