# Metamath Proof Explorer

## Theorem elixp

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

Ref Expression
Hypothesis elixp.1 ${⊢}{F}\in \mathrm{V}$
Assertion elixp ${⊢}{F}\in \underset{{x}\in {A}}{⨉}{B}↔\left({F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)$

### Proof

Step Hyp Ref Expression
1 elixp.1 ${⊢}{F}\in \mathrm{V}$
2 elixp2 ${⊢}{F}\in \underset{{x}\in {A}}{⨉}{B}↔\left({F}\in \mathrm{V}\wedge {F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)$
3 3anass ${⊢}\left({F}\in \mathrm{V}\wedge {F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)↔\left({F}\in \mathrm{V}\wedge \left({F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)\right)$
4 1 3 mpbiran ${⊢}\left({F}\in \mathrm{V}\wedge {F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)↔\left({F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)$
5 2 4 bitri ${⊢}{F}\in \underset{{x}\in {A}}{⨉}{B}↔\left({F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)$