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 ( ( 𝐹X 𝑥𝐴 𝐵𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 elixp2 ( 𝐹X 𝑥𝐴 𝐵 ↔ ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝐹𝑥 ) ∈ 𝐵 ) )
2 1 simp3bi ( 𝐹X 𝑥𝐴 𝐵 → ∀ 𝑥𝐴 ( 𝐹𝑥 ) ∈ 𝐵 )
3 2 r19.21bi ( ( 𝐹X 𝑥𝐴 𝐵𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ 𝐵 )