Metamath Proof Explorer

Theorem elixpconst

Description: Membership in an infinite Cartesian product of a constant B . (Contributed by NM, 12-Apr-2008)

Ref Expression
Hypothesis elixp.1 ⊢ F ∈ V
Assertion elixpconst ⊢ F ∈ ⨉ x ∈ A B ↔ F : A ⟶ B

Proof

Step Hyp Ref Expression
1 elixp.1 ⊢ F ∈ V
2 1 elixp ⊢ F ∈ ⨉ x ∈ A B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
3 ffnfv ⊢ F : A ⟶ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
4 2 3 bitr4i ⊢ F ∈ ⨉ x ∈ A B ↔ F : A ⟶ B