This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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