Theorem ralxpf

Description: Version of ralxp with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006) (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	ralxpf	$$⊢\forall x\in \left(A\times B\right)\phi \leftrightarrow \forall y\in A\forall 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		cbvralsvw	$$⊢\forall x\in \left(A\times B\right)\phi \leftrightarrow \forall w\in \left(A\times B\right)\left[w/x\right]\phi$$
6		cbvralsvw	$$⊢\forall z\in B\left[u/y\right]\psi \leftrightarrow \forall v\in B\left[v/z\right]\left[u/y\right]\psi$$
7	6	ralbii	$$⊢\forall u\in A\forall z\in B\left[u/y\right]\psi \leftrightarrow \forall u\in A\forall v\in B\left[v/z\right]\left[u/y\right]\psi$$
8		nfv	$$⊢Ⅎu\forall z\in B\psi$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
10		nfs1v	$$⊢Ⅎy\left[u/y\right]\psi$$
11	9 10	nfralw	$$⊢Ⅎy\forall z\in B\left[u/y\right]\psi$$
12		sbequ12	$$⊢y=u\to \left(\psi \leftrightarrow \left[u/y\right]\psi \right)$$
13	12	ralbidv	$$⊢y=u\to \left(\forall z\in B\psi \leftrightarrow \forall z\in B\left[u/y\right]\psi \right)$$
14	8 11 13	cbvralw	$$⊢\forall y\in A\forall z\in B\psi \leftrightarrow \forall u\in A\forall z\in B\left[u/y\right]\psi$$
15		vex	$$⊢u\in \mathrm{V}$$
16		vex	$$⊢v\in \mathrm{V}$$
17	15 16	eqvinop	$$⊢w=⟨u,v⟩\leftrightarrow \exists y\exists z\left(w=⟨y,z⟩\wedge ⟨y,z⟩=⟨u,v⟩\right)$$
18	1	nfsbv	$$⊢Ⅎy\left[w/x\right]\phi$$
19	10	nfsbv	$$⊢Ⅎy\left[v/z\right]\left[u/y\right]\psi$$
20	18 19	nfbi	$$⊢Ⅎy\left(\left[w/x\right]\phi \leftrightarrow \left[v/z\right]\left[u/y\right]\psi \right)$$
21	2	nfsbv	$$⊢Ⅎz\left[w/x\right]\phi$$
22		nfs1v	$$⊢Ⅎz\left[v/z\right]\left[u/y\right]\psi$$
23	21 22	nfbi	$$⊢Ⅎz\left(\left[w/x\right]\phi \leftrightarrow \left[v/z\right]\left[u/y\right]\psi \right)$$
24	3 4	sbhypf	$$⊢w=⟨y,z⟩\to \left(\left[w/x\right]\phi \leftrightarrow \psi \right)$$
25		vex	$$⊢y\in \mathrm{V}$$
26		vex	$$⊢z\in \mathrm{V}$$
27	25 26	opth	$$⊢⟨y,z⟩=⟨u,v⟩\leftrightarrow \left(y=u\wedge z=v\right)$$
28		sbequ12	$$⊢z=v\to \left(\left[u/y\right]\psi \leftrightarrow \left[v/z\right]\left[u/y\right]\psi \right)$$
29	12 28	sylan9bb	$$⊢\left(y=u\wedge z=v\right)\to \left(\psi \leftrightarrow \left[v/z\right]\left[u/y\right]\psi \right)$$
30	27 29	sylbi	$$⊢⟨y,z⟩=⟨u,v⟩\to \left(\psi \leftrightarrow \left[v/z\right]\left[u/y\right]\psi \right)$$
31	24 30	sylan9bb	$$⊢\left(w=⟨y,z⟩\wedge ⟨y,z⟩=⟨u,v⟩\right)\to \left(\left[w/x\right]\phi \leftrightarrow \left[v/z\right]\left[u/y\right]\psi \right)$$
32	23 31	exlimi	$$⊢\exists z\left(w=⟨y,z⟩\wedge ⟨y,z⟩=⟨u,v⟩\right)\to \left(\left[w/x\right]\phi \leftrightarrow \left[v/z\right]\left[u/y\right]\psi \right)$$
33	20 32	exlimi	$$⊢\exists y\exists z\left(w=⟨y,z⟩\wedge ⟨y,z⟩=⟨u,v⟩\right)\to \left(\left[w/x\right]\phi \leftrightarrow \left[v/z\right]\left[u/y\right]\psi \right)$$
34	17 33	sylbi	$$⊢w=⟨u,v⟩\to \left(\left[w/x\right]\phi \leftrightarrow \left[v/z\right]\left[u/y\right]\psi \right)$$
35	34	ralxp	$$⊢\forall w\in \left(A\times B\right)\left[w/x\right]\phi \leftrightarrow \forall u\in A\forall v\in B\left[v/z\right]\left[u/y\right]\psi$$
36	7 14 35	3bitr4ri	$$⊢\forall w\in \left(A\times B\right)\left[w/x\right]\phi \leftrightarrow \forall y\in A\forall z\in B\psi$$
37	5 36	bitri	$$⊢\forall x\in \left(A\times B\right)\phi \leftrightarrow \forall y\in A\forall z\in B\psi$$