Theorem nfixpw

Description: Bound-variable hypothesis builder for indexed Cartesian product. Version of nfixp with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 15-Oct-2016) (Revised by Gino Giotto, 26-Jan-2024)

	Ref	Expression
Hypotheses	nfixpw.1	$$⊢\underset{\_}{Ⅎ}yA$$
	nfixpw.2	$$⊢\underset{\_}{Ⅎ}yB$$
Assertion	nfixpw	$$⊢\underset{\_}{Ⅎ}y\underset{x\in A}{⨉}B$$

Proof

Step	Hyp	Ref	Expression
1		nfixpw.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		nfixpw.2	$$⊢\underset{\_}{Ⅎ}yB$$
3		df-ixp	$$⊢\underset{x\in A}{⨉}B=\left\{z|\left(zFn\left\{x|x\in A\right\}\wedge \forall x\in Az\left(x\right)\in B\right)\right\}$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}yz$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}yx$$
6	5 1	nfel	$$⊢Ⅎyx\in A$$
7	6	nfab	$$⊢\underset{\_}{Ⅎ}y\left\{x|x\in A\right\}$$
8	7	a1i	$$⊢\top \to \underset{\_}{Ⅎ}y\left\{x|x\in A\right\}$$
9	8	mptru	$$⊢\underset{\_}{Ⅎ}y\left\{x|x\in A\right\}$$
10	4 9	nffn	$$⊢ℲyzFn\left\{x|x\in A\right\}$$
11		df-ral	$$⊢\forall x\in Az\left(x\right)\in B\leftrightarrow \forall x\left(x\in A\to z\left(x\right)\in B\right)$$
12		nftru	$$⊢Ⅎx\top$$
13	6	a1i	$$⊢\top \to Ⅎyx\in A$$
14	4	a1i	$$⊢\top \to \underset{\_}{Ⅎ}yz$$
15	5	a1i	$$⊢\top \to \underset{\_}{Ⅎ}yx$$
16	14 15	nffvd	$$⊢\top \to \underset{\_}{Ⅎ}yz\left(x\right)$$
17	2	a1i	$$⊢\top \to \underset{\_}{Ⅎ}yB$$
18	16 17	nfeld	$$⊢\top \to Ⅎyz\left(x\right)\in B$$
19	13 18	nfimd	$$⊢\top \to Ⅎy\left(x\in A\to z\left(x\right)\in B\right)$$
20	12 19	nfald	$$⊢\top \to Ⅎy\forall x\left(x\in A\to z\left(x\right)\in B\right)$$
21	20	mptru	$$⊢Ⅎy\forall x\left(x\in A\to z\left(x\right)\in B\right)$$
22	11 21	nfxfr	$$⊢Ⅎy\forall x\in Az\left(x\right)\in B$$
23	10 22	nfan	$$⊢Ⅎy\left(zFn\left\{x|x\in A\right\}\wedge \forall x\in Az\left(x\right)\in B\right)$$
24	23	nfab	$$⊢\underset{\_}{Ⅎ}y\left\{z|\left(zFn\left\{x|x\in A\right\}\wedge \forall x\in Az\left(x\right)\in B\right)\right\}$$
25	3 24	nfcxfr	$$⊢\underset{\_}{Ⅎ}y\underset{x\in A}{⨉}B$$