Theorem resfunexgALT

Description: Alternate proof of resfunexg , shorter but requiring ax-pow and ax-un . (Contributed by NM, 7-Apr-1995) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	resfunexgALT	⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ↾ 𝐵 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		dmresexg	⊢ ( 𝐵 ∈ 𝐶 → dom ( 𝐴 ↾ 𝐵 ) ∈ V )
2	1	adantl	⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → dom ( 𝐴 ↾ 𝐵 ) ∈ V )
3		df-ima	⊢ ( 𝐴 “ 𝐵 ) = ran ( 𝐴 ↾ 𝐵 )
4		funimaexg	⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 “ 𝐵 ) ∈ V )
5	3 4	eqeltrrid	⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ran ( 𝐴 ↾ 𝐵 ) ∈ V )
6	2 5	jca	⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( dom ( 𝐴 ↾ 𝐵 ) ∈ V ∧ ran ( 𝐴 ↾ 𝐵 ) ∈ V ) )
7		xpexg	⊢ ( ( dom ( 𝐴 ↾ 𝐵 ) ∈ V ∧ ran ( 𝐴 ↾ 𝐵 ) ∈ V ) → ( dom ( 𝐴 ↾ 𝐵 ) × ran ( 𝐴 ↾ 𝐵 ) ) ∈ V )
8		relres	⊢ Rel ( 𝐴 ↾ 𝐵 )
9		relssdmrn	⊢ ( Rel ( 𝐴 ↾ 𝐵 ) → ( 𝐴 ↾ 𝐵 ) ⊆ ( dom ( 𝐴 ↾ 𝐵 ) × ran ( 𝐴 ↾ 𝐵 ) ) )
10	8 9	ax-mp	⊢ ( 𝐴 ↾ 𝐵 ) ⊆ ( dom ( 𝐴 ↾ 𝐵 ) × ran ( 𝐴 ↾ 𝐵 ) )
11		ssexg	⊢ ( ( ( 𝐴 ↾ 𝐵 ) ⊆ ( dom ( 𝐴 ↾ 𝐵 ) × ran ( 𝐴 ↾ 𝐵 ) ) ∧ ( dom ( 𝐴 ↾ 𝐵 ) × ran ( 𝐴 ↾ 𝐵 ) ) ∈ V ) → ( 𝐴 ↾ 𝐵 ) ∈ V )
12	10 11	mpan	⊢ ( ( dom ( 𝐴 ↾ 𝐵 ) × ran ( 𝐴 ↾ 𝐵 ) ) ∈ V → ( 𝐴 ↾ 𝐵 ) ∈ V )
13	6 7 12	3syl	⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ↾ 𝐵 ) ∈ V )