This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iunrab

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

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

Proof

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