Theorem nfixp

Description: Bound-variable hypothesis builder for indexed Cartesian product. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfixpw when possible. (Contributed by Mario Carneiro, 15-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfixp.1	|- F/_ y A
	nfixp.2	|- F/_ y B
Assertion	nfixp	|- F/_ y X_ x e. A B

Proof

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