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

Metamath Proof Explorer

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) Avoid ax-13 . (Revised by GG, 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