Metamath Proof Explorer


Theorem elixp

Description: Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006)

Ref Expression
Hypothesis elixp.1 F V
Assertion elixp F x A B F Fn A x A F x B

Proof

Step Hyp Ref Expression
1 elixp.1 F V
2 elixp2 F x A B F V F Fn A x A F x B
3 3anass F V F Fn A x A F x B F V F Fn A x A F x B
4 1 3 mpbiran F V F Fn A x A F x B F Fn A x A F x B
5 2 4 bitri F x A B F Fn A x A F x B