Theorem iunrab 5052

Description: The indexed union of a restricted class abstraction. (Contributed by NM, 3-Jan-2004.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)

Assertion

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

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

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑦)

Proof of Theorem iunrab

Step	Hyp	Ref	Expression
1		iunab 5051	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝜑)} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑)}
2		df-rab 3437	. . . 4 ⊢ {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝜑)}
3	2	a1i 11	. . 3 ⊢ (𝑥 ∈ 𝐴 → {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝜑)})
4	3	iuneq2i 5013	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝜑)}
5		df-rab 3437	. . 3 ⊢ {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝐴 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑)}
6		r19.42v 3191	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑))
7	6	abbii 2809	. . 3 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑)}
8	5, 7	eqtr4i 2768	. 2 ⊢ {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝐴 𝜑} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑)}
9	1, 4, 8	3eqtr4i 2775	1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝐴 𝜑}

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {cab 2714  ∃wrex 3070  {crab 3436  ∪ ciun 4991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-ss 3968  df-iun 4993

This theorem is referenced by:  hashrabrex  15861  incexc2  15874  phisum  16828  itg2monolem1  25785  aannenlem1  26370  musum  27234  lgsquadlem1  27424  lgsquadlem2  27425  edglnl  29160  rabrexfi  32525  iunpreima  32577  poimirlem27  37654  cnambfre  37675  mapdval3N  41633  mapdval5N  41635  fiphp3d  42830