Metamath Proof Explorer

Theorem iunopab

Description: Move indexed union inside an ordered-pair class abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015)

		Ref	Expression
	Assertion	iunopab	$⊢ ⋃_{z \in A} \{⟨x, y⟩ \| φ\} = \{⟨x, y⟩ \| \exists z \in A φ\}$

Proof

Step	Hyp	Ref	Expression
1		elopab	$⊢ w \in \{⟨x, y⟩ \| φ\} \leftrightarrow \exists x \exists y (w = ⟨x, y⟩ \land φ)$
2	1	rexbii	$⊢ \exists z \in A w \in \{⟨x, y⟩ \| φ\} \leftrightarrow \exists z \in A \exists x \exists y (w = ⟨x, y⟩ \land φ)$
3		rexcom4	$⊢ \exists z \in A \exists x \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists z \in A \exists y (w = ⟨x, y⟩ \land φ)$
4		rexcom4	$⊢ \exists z \in A \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists y \exists z \in A (w = ⟨x, y⟩ \land φ)$
5		r19.42v	$⊢ \exists z \in A (w = ⟨x, y⟩ \land φ) \leftrightarrow (w = ⟨x, y⟩ \land \exists z \in A φ)$
6	5	exbii	$⊢ \exists y \exists z \in A (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists y (w = ⟨x, y⟩ \land \exists z \in A φ)$
7	4 6	bitri	$⊢ \exists z \in A \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists y (w = ⟨x, y⟩ \land \exists z \in A φ)$
8	7	exbii	$⊢ \exists x \exists z \in A \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y (w = ⟨x, y⟩ \land \exists z \in A φ)$
9	3 8	bitri	$⊢ \exists z \in A \exists x \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y (w = ⟨x, y⟩ \land \exists z \in A φ)$
10	2 9	bitri	$⊢ \exists z \in A w \in \{⟨x, y⟩ \| φ\} \leftrightarrow \exists x \exists y (w = ⟨x, y⟩ \land \exists z \in A φ)$
11	10	abbii	$⊢ \{w \| \exists z \in A w \in \{⟨x, y⟩ \| φ\}\} = \{w \| \exists x \exists y (w = ⟨x, y⟩ \land \exists z \in A φ)\}$
12		df-iun	$⊢ ⋃_{z \in A} \{⟨x, y⟩ \| φ\} = \{w \| \exists z \in A w \in \{⟨x, y⟩ \| φ\}\}$
13		df-opab	$⊢ \{⟨x, y⟩ \| \exists z \in A φ\} = \{w \| \exists x \exists y (w = ⟨x, y⟩ \land \exists z \in A φ)\}$
14	11 12 13	3eqtr4i	$⊢ ⋃_{z \in A} \{⟨x, y⟩ \| φ\} = \{⟨x, y⟩ \| \exists z \in A φ\}$