Theorem nfixp1

Description: The index variable in an indexed Cartesian product is not free. (Contributed by Jeff Madsen, 19-Jun-2011) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Assertion	nfixp1	⊢ Ⅎ 𝑥 X 𝑥 ∈ 𝐴 𝐵

Proof

Step	Hyp	Ref	Expression
1		df-ixp	⊢ X 𝑥 ∈ 𝐴 𝐵 = { 𝑦 ∣ ( 𝑦 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ‘ 𝑥 ) ∈ 𝐵 ) }
2		nfcv	⊢ Ⅎ 𝑥 𝑦
3		nfab1	⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝑥 ∈ 𝐴 }
4	2 3	nffn	⊢ Ⅎ 𝑥 𝑦 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 }
5		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 ( 𝑦 ‘ 𝑥 ) ∈ 𝐵
6	4 5	nfan	⊢ Ⅎ 𝑥 ( 𝑦 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ‘ 𝑥 ) ∈ 𝐵 )
7	6	nfab	⊢ Ⅎ 𝑥 { 𝑦 ∣ ( 𝑦 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ‘ 𝑥 ) ∈ 𝐵 ) }
8	1 7	nfcxfr	⊢ Ⅎ 𝑥 X 𝑥 ∈ 𝐴 𝐵