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