Theorem iunrab 4983

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 4982	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝜑)} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑)}
2		df-rab 3392	. . . 4 ⊢ {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝜑)}
3	2	a1i 11	. . 3 ⊢ (𝑥 ∈ 𝐴 → {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝜑)})
4	3	iuneq2i 4944	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ 𝜑)}
5		df-rab 3392	. . 3 ⊢ {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝐴 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑)}
6		r19.42v 3171	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑))
7	6	abbii 2806	. . 3 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑)}
8	5, 7	eqtr4i 2765	. 2 ⊢ {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝐴 𝜑} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝜑)}
9	1, 4, 8	3eqtr4i 2772	1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝐴 𝜑}

Syntax hints:   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {cab 2717  ∃wrex 3063  {crab 3391  ∪ ciun 4922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-ss 3900  df-iun 4924

This theorem is referenced by:  hashrabrex  15780  incexc2  15795  phisum  16753  chnfi  18592  itg2monolem1  25736  aannenlem1  26313  musum  27173  lgsquadlem1  27362  lgsquadlem2  27363  edglnl  29231  rabrexfi  32595  iunpreima  32654  poimirlem27  38023  cnambfre  38044  mapdval3N  42132  mapdval5N  42134  fiphp3d  43273