Theorem elixpconst

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

	Ref	Expression
Hypothesis	elixp.1	⊢ 𝐹 ∈ V
Assertion	elixpconst	⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elixp.1	⊢ 𝐹 ∈ V
2	1	elixp	⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
3		ffnfv	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
4	2 3	bitr4i	⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )