mapval2

Description: Alternate expression for the value of set exponentiation. (Contributed by NM, 3-Nov-2007)

Step	Hyp	Ref	Expression
1		elmap.1	$⊢ A \in V$
2		elmap.2	$⊢ B \in V$
3		dff2	$⊢ g : B ⟶ A \leftrightarrow (g Fn B \land g \subseteq B \times A)$
4	3	biancomi	$⊢ g : B ⟶ A \leftrightarrow (g \subseteq B \times A \land g Fn B)$
5	1 2	elmap	$⊢ g \in (A^{B}) \leftrightarrow g : B ⟶ A$
6		elin	$⊢ g \in (𝒫 (B \times A) \cap \{f \| f Fn B\}) \leftrightarrow (g \in 𝒫 (B \times A) \land g \in \{f \| f Fn B\})$
7		velpw	$⊢ g \in 𝒫 (B \times A) \leftrightarrow g \subseteq B \times A$
8		vex	$⊢ g \in V$
9		fneq1	$⊢ f = g \to (f Fn B \leftrightarrow g Fn B)$
10	8 9	elab	$⊢ g \in \{f \| f Fn B\} \leftrightarrow g Fn B$
11	7 10	anbi12i	$⊢ (g \in 𝒫 (B \times A) \land g \in \{f \| f Fn B\}) \leftrightarrow (g \subseteq B \times A \land g Fn B)$
12	6 11	bitri	$⊢ g \in (𝒫 (B \times A) \cap \{f \| f Fn B\}) \leftrightarrow (g \subseteq B \times A \land g Fn B)$
13	4 5 12	3bitr4i	$⊢ g \in (A^{B}) \leftrightarrow g \in (𝒫 (B \times A) \cap \{f \| f Fn B\})$
14	13	eqriv	$⊢ A^{B} = 𝒫 (B \times A) \cap \{f \| f Fn B\}$

Metamath Proof Explorer