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 ⊢ ⋃ x ∈ A y ∈ B | φ = y ∈ B | ∃ x ∈ A φ

Proof

Step Hyp Ref Expression
1 iunab ⊢ ⋃ x ∈ A y | y ∈ B ∧ φ = y | ∃ x ∈ A y ∈ B ∧ φ
2 df-rab ⊢ y ∈ B | φ = y | y ∈ B ∧ φ
3 2 a1i ⊢ x ∈ A → y ∈ B | φ = y | y ∈ B ∧ φ
4 3 iuneq2i ⊢ ⋃ x ∈ A y ∈ B | φ = ⋃ x ∈ A y | y ∈ B ∧ φ
5 df-rab ⊢ y ∈ B | ∃ x ∈ A φ = y | y ∈ B ∧ ∃ x ∈ A φ
6 r19.42v ⊢ ∃ x ∈ A y ∈ B ∧ φ ↔ y ∈ B ∧ ∃ x ∈ A φ
7 6 abbii ⊢ y | ∃ x ∈ A y ∈ B ∧ φ = y | y ∈ B ∧ ∃ x ∈ A φ
8 5 7 eqtr4i ⊢ y ∈ B | ∃ x ∈ A φ = y | ∃ x ∈ A y ∈ B ∧ φ
9 1 4 8 3eqtr4i ⊢ ⋃ x ∈ A y ∈ B | φ = y ∈ B | ∃ x ∈ A φ