Theorem mapval2

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

	Ref	Expression
Hypotheses	elmap.1	|- A e. _V
	elmap.2	|- B e. _V
Assertion	mapval2	|- ( A ^m B ) = ( ~P ( B X. A ) i^i { f | f Fn B } )

Proof

Step	Hyp	Ref	Expression
1		elmap.1	|- A e. _V
2		elmap.2	|- B e. _V
3		dff2	|- ( g : B --> A <-> ( g Fn B /\ g C_ ( B X. A ) ) )
4	3	biancomi	|- ( g : B --> A <-> ( g C_ ( B X. A ) /\ g Fn B ) )
5	1 2	elmap	|- ( g e. ( A ^m B ) <-> g : B --> A )
6		elin	|- ( g e. ( ~P ( B X. A ) i^i { f | f Fn B } ) <-> ( g e. ~P ( B X. A ) /\ g e. { f | f Fn B } ) )
7		velpw	|- ( g e. ~P ( B X. A ) <-> g C_ ( B X. A ) )
8		vex	|- g e. _V
9		fneq1	|- ( f = g -> ( f Fn B <-> g Fn B ) )
10	8 9	elab	|- ( g e. { f | f Fn B } <-> g Fn B )
11	7 10	anbi12i	|- ( ( g e. ~P ( B X. A ) /\ g e. { f | f Fn B } ) <-> ( g C_ ( B X. A ) /\ g Fn B ) )
12	6 11	bitri	|- ( g e. ( ~P ( B X. A ) i^i { f | f Fn B } ) <-> ( g C_ ( B X. A ) /\ g Fn B ) )
13	4 5 12	3bitr4i	|- ( g e. ( A ^m B ) <-> g e. ( ~P ( B X. A ) i^i { f | f Fn B } ) )
14	13	eqriv	|- ( A ^m B ) = ( ~P ( B X. A ) i^i { f | f Fn B } )