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 e. X_ x e. A B /\ x e. A ) -> ( F ` x ) e. B )

Proof

Step Hyp Ref Expression
1 elixp2 
 |-  ( F e. X_ x e. A B <-> ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) )
2 1 simp3bi 
 |-  ( F e. X_ x e. A B -> A. x e. A ( F ` x ) e. B )
3 2 r19.21bi 
 |-  ( ( F e. X_ x e. A B /\ x e. A ) -> ( F ` x ) e. B )