fvixp

Description: Projection of a factor of an indexed Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016)

		Ref	Expression
	Hypothesis	fvixp.1	$⊢ x = C \to B = D$
	Assertion	fvixp	$⊢ (F \in \underset{x \in A}{⨉} B \land C \in A) \to F (C) \in D$

Step	Hyp	Ref	Expression
1		fvixp.1	$⊢ x = C \to B = D$
2		elixp2	$⊢ F \in \underset{x \in A}{⨉} B \leftrightarrow (F \in V \land F Fn A \land \forall x \in A F (x) \in B)$
3	2	simp3bi	$⊢ F \in \underset{x \in A}{⨉} B \to \forall x \in A F (x) \in B$
4		fveq2	$⊢ x = C \to F (x) = F (C)$
5	4 1	eleq12d	$⊢ x = C \to (F (x) \in B \leftrightarrow F (C) \in D)$
6	5	rspccva	$⊢ (\forall x \in A F (x) \in B \land C \in A) \to F (C) \in D$
7	3 6	sylan	$⊢ (F \in \underset{x \in A}{⨉} B \land C \in A) \to F (C) \in D$

Metamath Proof Explorer