Metamath Proof Explorer

Theorem fvixp2

Description: Projection of a factor of an indexed Cartesian product. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Assertion fvixp2 ⊢ F ∈ ⨉ x ∈ A B ∧ x ∈ A → F ⁡ x ∈ B

Proof

Step Hyp Ref Expression
1 elixp2 ⊢ F ∈ ⨉ x ∈ A B ↔ F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
2 1 simp3bi ⊢ F ∈ ⨉ x ∈ A B → ∀ x ∈ A F ⁡ x ∈ B
3 2 r19.21bi ⊢ F ∈ ⨉ x ∈ A B ∧ x ∈ A → F ⁡ x ∈ B