Theorem rexxpf

Description: Version of rexxp with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	ralxpf.1	$$⊢Ⅎy\phi$$
	ralxpf.2	$$⊢Ⅎz\phi$$
	ralxpf.3	$$⊢Ⅎx\psi$$
	ralxpf.4	$$⊢x=⟨y,z⟩\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	rexxpf	$$⊢\exists x\in \left(A\times B\right)\phi \leftrightarrow \exists y\in A\exists z\in B\psi$$

Proof

Step	Hyp	Ref	Expression
1		ralxpf.1	$$⊢Ⅎy\phi$$
2		ralxpf.2	$$⊢Ⅎz\phi$$
3		ralxpf.3	$$⊢Ⅎx\psi$$
4		ralxpf.4	$$⊢x=⟨y,z⟩\to \left(\phi \leftrightarrow \psi \right)$$
5	1	nfn	$$⊢Ⅎy\neg \phi$$
6	2	nfn	$$⊢Ⅎz\neg \phi$$
7	3	nfn	$$⊢Ⅎx\neg \psi$$
8	4	notbid	$$⊢x=⟨y,z⟩\to \left(\neg \phi \leftrightarrow \neg \psi \right)$$
9	5 6 7 8	ralxpf	$$⊢\forall x\in \left(A\times B\right)\neg \phi \leftrightarrow \forall y\in A\forall z\in B\neg \psi$$
10		ralnex	$$⊢\forall z\in B\neg \psi \leftrightarrow \neg \exists z\in B\psi$$
11	10	ralbii	$$⊢\forall y\in A\forall z\in B\neg \psi \leftrightarrow \forall y\in A\neg \exists z\in B\psi$$
12	9 11	bitri	$$⊢\forall x\in \left(A\times B\right)\neg \phi \leftrightarrow \forall y\in A\neg \exists z\in B\psi$$
13	12	notbii	$$⊢\neg \forall x\in \left(A\times B\right)\neg \phi \leftrightarrow \neg \forall y\in A\neg \exists z\in B\psi$$
14		dfrex2	$$⊢\exists x\in \left(A\times B\right)\phi \leftrightarrow \neg \forall x\in \left(A\times B\right)\neg \phi$$
15		dfrex2	$$⊢\exists y\in A\exists z\in B\psi \leftrightarrow \neg \forall y\in A\neg \exists z\in B\psi$$
16	13 14 15	3bitr4i	$$⊢\exists x\in \left(A\times B\right)\phi \leftrightarrow \exists y\in A\exists z\in B\psi$$