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

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