elixp

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

		Ref	Expression
	Hypothesis	elixp.1	$⊢ F \in V$
	Assertion	elixp	$⊢ F \in \underset{x \in A}{⨉} B \leftrightarrow (F Fn A \land \forall x \in A F (x) \in B)$

Step	Hyp	Ref	Expression
1		elixp.1	$⊢ F \in V$
2		elixp2	$⊢ F \in \underset{x \in A}{⨉} B \leftrightarrow (F \in V \land F Fn A \land \forall x \in A F (x) \in B)$
3		3anass	$⊢ (F \in V \land F Fn A \land \forall x \in A F (x) \in B) \leftrightarrow (F \in V \land (F Fn A \land \forall x \in A F (x) \in B))$
4	1 3	mpbiran	$⊢ (F \in V \land F Fn A \land \forall x \in A F (x) \in B) \leftrightarrow (F Fn A \land \forall x \in A F (x) \in B)$
5	2 4	bitri	$⊢ F \in \underset{x \in A}{⨉} B \leftrightarrow (F Fn A \land \forall x \in A F (x) \in B)$

Metamath Proof Explorer