Theorem rexiunxp

Description: Write a double restricted quantification as one universal quantifier. In this version of rexxp , B ( y ) is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015)

	Ref	Expression
Hypothesis	ralxp.1	$$⊢x=⟨y,z⟩\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	rexiunxp	$$⊢\exists x\in \bigcup _{y\in A}\left(\left\{y\right\}\times B\right)\phi \leftrightarrow \exists y\in A\exists z\in B\psi$$

Proof

Step	Hyp	Ref	Expression
1		ralxp.1	$$⊢x=⟨y,z⟩\to \left(\phi \leftrightarrow \psi \right)$$
2	1	notbid	$$⊢x=⟨y,z⟩\to \left(\neg \phi \leftrightarrow \neg \psi \right)$$
3	2	raliunxp	$$⊢\forall x\in \bigcup _{y\in A}\left(\left\{y\right\}\times B\right)\neg \phi \leftrightarrow \forall y\in A\forall z\in B\neg \psi$$
4		ralnex	$$⊢\forall z\in B\neg \psi \leftrightarrow \neg \exists z\in B\psi$$
5	4	ralbii	$$⊢\forall y\in A\forall z\in B\neg \psi \leftrightarrow \forall y\in A\neg \exists z\in B\psi$$
6	3 5	bitri	$$⊢\forall x\in \bigcup _{y\in A}\left(\left\{y\right\}\times B\right)\neg \phi \leftrightarrow \forall y\in A\neg \exists z\in B\psi$$
7	6	notbii	$$⊢\neg \forall x\in \bigcup _{y\in A}\left(\left\{y\right\}\times B\right)\neg \phi \leftrightarrow \neg \forall y\in A\neg \exists z\in B\psi$$
8		dfrex2	$$⊢\exists x\in \bigcup _{y\in A}\left(\left\{y\right\}\times B\right)\phi \leftrightarrow \neg \forall x\in \bigcup _{y\in A}\left(\left\{y\right\}\times B\right)\neg \phi$$
9		dfrex2	$$⊢\exists y\in A\exists z\in B\psi \leftrightarrow \neg \forall y\in A\neg \exists z\in B\psi$$
10	7 8 9	3bitr4i	$$⊢\exists x\in \bigcup _{y\in A}\left(\left\{y\right\}\times B\right)\phi \leftrightarrow \exists y\in A\exists z\in B\psi$$