Theorem fnexALT

Description: Alternate proof of fnex , derived using the Axiom of Replacement in the form of funimaexg . This version uses ax-pow and ax-un , whereas fnex does not. (Contributed by NM, 14-Aug-1994) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	fnexALT	|- ( ( F Fn A /\ A e. B ) -> F e. _V )

Proof

Step	Hyp	Ref	Expression
1		fnrel	|- ( F Fn A -> Rel F )
2		relssdmrn	|- ( Rel F -> F C_ ( dom F X. ran F ) )
3	1 2	syl	|- ( F Fn A -> F C_ ( dom F X. ran F ) )
4	3	adantr	|- ( ( F Fn A /\ A e. B ) -> F C_ ( dom F X. ran F ) )
5		fndm	|- ( F Fn A -> dom F = A )
6	5	eleq1d	|- ( F Fn A -> ( dom F e. B <-> A e. B ) )
7	6	biimpar	|- ( ( F Fn A /\ A e. B ) -> dom F e. B )
8		fnfun	|- ( F Fn A -> Fun F )
9		funimaexg	|- ( ( Fun F /\ A e. B ) -> ( F " A ) e. _V )
10	8 9	sylan	|- ( ( F Fn A /\ A e. B ) -> ( F " A ) e. _V )
11		imadmrn	|- ( F " dom F ) = ran F
12	5	imaeq2d	|- ( F Fn A -> ( F " dom F ) = ( F " A ) )
13	11 12	eqtr3id	|- ( F Fn A -> ran F = ( F " A ) )
14	13	eleq1d	|- ( F Fn A -> ( ran F e. _V <-> ( F " A ) e. _V ) )
15	14	biimpar	|- ( ( F Fn A /\ ( F " A ) e. _V ) -> ran F e. _V )
16	10 15	syldan	|- ( ( F Fn A /\ A e. B ) -> ran F e. _V )
17		xpexg	|- ( ( dom F e. B /\ ran F e. _V ) -> ( dom F X. ran F ) e. _V )
18	7 16 17	syl2anc	|- ( ( F Fn A /\ A e. B ) -> ( dom F X. ran F ) e. _V )
19		ssexg	|- ( ( F C_ ( dom F X. ran F ) /\ ( dom F X. ran F ) e. _V ) -> F e. _V )
20	4 18 19	syl2anc	|- ( ( F Fn A /\ A e. B ) -> F e. _V )