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	|- F/_ y A
	nfixpw.2	|- F/_ y B
Assertion	nfixpw	|- F/_ y X_ x e. A B

Proof

Step	Hyp	Ref	Expression
1		nfixpw.1	|- F/_ y A
2		nfixpw.2	|- F/_ y B
3		df-ixp	|- X_ x e. A B = { z | ( z Fn { x | x e. A } /\ A. x e. A ( z ` x ) e. B ) }
4		nfcv	|- F/_ y z
5		nfcv	|- F/_ y x
6	5 1	nfel	|- F/ y x e. A
7	6	nfab	|- F/_ y { x | x e. A }
8	7	a1i	|- ( T. -> F/_ y { x | x e. A } )
9	8	mptru	|- F/_ y { x | x e. A }
10	4 9	nffn	|- F/ y z Fn { x | x e. A }
11		df-ral	|- ( A. x e. A ( z ` x ) e. B <-> A. x ( x e. A -> ( z ` x ) e. B ) )
12		nftru	|- F/ x T.
13	6	a1i	|- ( T. -> F/ y x e. A )
14	4	a1i	|- ( T. -> F/_ y z )
15	5	a1i	|- ( T. -> F/_ y x )
16	14 15	nffvd	|- ( T. -> F/_ y ( z ` x ) )
17	2	a1i	|- ( T. -> F/_ y B )
18	16 17	nfeld	|- ( T. -> F/ y ( z ` x ) e. B )
19	13 18	nfimd	|- ( T. -> F/ y ( x e. A -> ( z ` x ) e. B ) )
20	12 19	nfald	|- ( T. -> F/ y A. x ( x e. A -> ( z ` x ) e. B ) )
21	20	mptru	|- F/ y A. x ( x e. A -> ( z ` x ) e. B )
22	11 21	nfxfr	|- F/ y A. x e. A ( z ` x ) e. B
23	10 22	nfan	|- F/ y ( z Fn { x | x e. A } /\ A. x e. A ( z ` x ) e. B )
24	23	nfab	|- F/_ y { z | ( z Fn { x | x e. A } /\ A. x e. A ( z ` x ) e. B ) }
25	3 24	nfcxfr	|- F/_ y X_ x e. A B