Theorem iunopab

Description: Move indexed union inside an ordered-pair class abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015) Avoid ax-sep , ax-nul , ax-pr . (Revised by SN, 11-Nov-2024)

	Ref	Expression
Assertion	iunopab	$$⊢\bigcup _{z\in A}\left\{⟨x,y⟩|\phi \right\}=\left\{⟨x,y⟩|\exists z\in A\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		elopabw	$$⊢w\in \mathrm{V}\to \left(w\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right)$$
2	1	elv	$$⊢w\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)$$
3	2	rexbii	$$⊢\exists z\in Aw\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists z\in A\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)$$
4		rexcom4	$$⊢\exists z\in A\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists z\in A\exists y\left(w=⟨x,y⟩\wedge \phi \right)$$
5		rexcom4	$$⊢\exists z\in A\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists y\exists z\in A\left(w=⟨x,y⟩\wedge \phi \right)$$
6		r19.42v	$$⊢\exists z\in A\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(w=⟨x,y⟩\wedge \exists z\in A\phi \right)$$
7	6	exbii	$$⊢\exists y\exists z\in A\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists y\left(w=⟨x,y⟩\wedge \exists z\in A\phi \right)$$
8	5 7	bitri	$$⊢\exists z\in A\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists y\left(w=⟨x,y⟩\wedge \exists z\in A\phi \right)$$
9	8	exbii	$$⊢\exists x\exists z\in A\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\left(w=⟨x,y⟩\wedge \exists z\in A\phi \right)$$
10	4 9	bitri	$$⊢\exists z\in A\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\left(w=⟨x,y⟩\wedge \exists z\in A\phi \right)$$
11	3 10	bitri	$$⊢\exists z\in Aw\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(w=⟨x,y⟩\wedge \exists z\in A\phi \right)$$
12	11	abbii	$$⊢\left\{w|\exists z\in Aw\in \left\{⟨x,y⟩|\phi \right\}\right\}=\left\{w|\exists x\exists y\left(w=⟨x,y⟩\wedge \exists z\in A\phi \right)\right\}$$
13		df-iun	$$⊢\bigcup _{z\in A}\left\{⟨x,y⟩|\phi \right\}=\left\{w|\exists z\in Aw\in \left\{⟨x,y⟩|\phi \right\}\right\}$$
14		df-opab	$$⊢\left\{⟨x,y⟩|\exists z\in A\phi \right\}=\left\{w|\exists x\exists y\left(w=⟨x,y⟩\wedge \exists z\in A\phi \right)\right\}$$
15	12 13 14	3eqtr4i	$$⊢\bigcup _{z\in A}\left\{⟨x,y⟩|\phi \right\}=\left\{⟨x,y⟩|\exists z\in A\phi \right\}$$