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

Metamath Proof Explorer

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	$⊢ \underline{Ⅎ} x \underset{x \in A}{⨉} B$

Proof

Step	Hyp	Ref	Expression
1		df-ixp	$⊢ \underset{x \in A}{⨉} B = \{y \| (y Fn \{x \| x \in A\} \land \forall x \in A y (x) \in B)\}$
2		nfcv	$⊢ \underline{Ⅎ} x y$
3		nfab1	$⊢ \underline{Ⅎ} x \{x \| x \in A\}$
4	2 3	nffn	$⊢ Ⅎ x y Fn \{x \| x \in A\}$
5		nfra1	$⊢ Ⅎ x \forall x \in A y (x) \in B$
6	4 5	nfan	$⊢ Ⅎ x (y Fn \{x \| x \in A\} \land \forall x \in A y (x) \in B)$
7	6	nfab	$⊢ \underline{Ⅎ} x \{y \| (y Fn \{x \| x \in A\} \land \forall x \in A y (x) \in B)\}$
8	1 7	nfcxfr	$⊢ \underline{Ⅎ} x \underset{x \in A}{⨉} B$