Theorem elixp

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

	Ref	Expression
Hypothesis	elixp.1	⊢ 𝐹 ∈ V
Assertion	elixp	⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elixp.1	⊢ 𝐹 ∈ V
2		elixp2	⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
3		3anass	⊢ ( ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ↔ ( 𝐹 ∈ V ∧ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ) )
4	1 3	mpbiran	⊢ ( ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
5	2 4	bitri	⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )