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	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵 ) → 𝐹 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		fnrel	⊢ ( 𝐹 Fn 𝐴 → Rel 𝐹 )
2		relssdmrn	⊢ ( Rel 𝐹 → 𝐹 ⊆ ( dom 𝐹 × ran 𝐹 ) )
3	1 2	syl	⊢ ( 𝐹 Fn 𝐴 → 𝐹 ⊆ ( dom 𝐹 × ran 𝐹 ) )
4	3	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵 ) → 𝐹 ⊆ ( dom 𝐹 × ran 𝐹 ) )
5		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
6	5	eleq1d	⊢ ( 𝐹 Fn 𝐴 → ( dom 𝐹 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
7	6	biimpar	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵 ) → dom 𝐹 ∈ 𝐵 )
8		fnfun	⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
9		funimaexg	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐹 “ 𝐴 ) ∈ V )
10	8 9	sylan	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐹 “ 𝐴 ) ∈ V )
11		imadmrn	⊢ ( 𝐹 “ dom 𝐹 ) = ran 𝐹
12	5	imaeq2d	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 “ dom 𝐹 ) = ( 𝐹 “ 𝐴 ) )
13	11 12	eqtr3id	⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = ( 𝐹 “ 𝐴 ) )
14	13	eleq1d	⊢ ( 𝐹 Fn 𝐴 → ( ran 𝐹 ∈ V ↔ ( 𝐹 “ 𝐴 ) ∈ V ) )
15	14	biimpar	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐹 “ 𝐴 ) ∈ V ) → ran 𝐹 ∈ V )
16	10 15	syldan	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵 ) → ran 𝐹 ∈ V )
17		xpexg	⊢ ( ( dom 𝐹 ∈ 𝐵 ∧ ran 𝐹 ∈ V ) → ( dom 𝐹 × ran 𝐹 ) ∈ V )
18	7 16 17	syl2anc	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵 ) → ( dom 𝐹 × ran 𝐹 ) ∈ V )
19		ssexg	⊢ ( ( 𝐹 ⊆ ( dom 𝐹 × ran 𝐹 ) ∧ ( dom 𝐹 × ran 𝐹 ) ∈ V ) → 𝐹 ∈ V )
20	4 18 19	syl2anc	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵 ) → 𝐹 ∈ V )