Metamath Proof Explorer

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 A \land B \in C) \to {A ↾}_{B} \in V$

Proof

Step	Hyp	Ref	Expression
1		dmresexg	$⊢ B \in C \to dom ({A ↾}_{B}) \in V$
2	1	adantl	$⊢ (Fun A \land B \in C) \to dom ({A ↾}_{B}) \in V$
3		df-ima	$⊢ A [B] = ran ({A ↾}_{B})$
4		funimaexg	$⊢ (Fun A \land B \in C) \to A [B] \in V$
5	3 4	eqeltrrid	$⊢ (Fun A \land B \in C) \to ran ({A ↾}_{B}) \in V$
6	2 5	jca	$⊢ (Fun A \land B \in C) \to (dom ({A ↾}_{B}) \in V \land ran ({A ↾}_{B}) \in V)$
7		xpexg	$⊢ (dom ({A ↾}_{B}) \in V \land ran ({A ↾}_{B}) \in V) \to dom ({A ↾}_{B}) \times ran ({A ↾}_{B}) \in V$
8		relres	$⊢ Rel ({A ↾}_{B})$
9		relssdmrn	$⊢ Rel ({A ↾}_{B}) \to {A ↾}_{B} \subseteq dom ({A ↾}_{B}) \times ran ({A ↾}_{B})$
10	8 9	ax-mp	$⊢ {A ↾}_{B} \subseteq dom ({A ↾}_{B}) \times ran ({A ↾}_{B})$
11		ssexg	$⊢ ({A ↾}_{B} \subseteq dom ({A ↾}_{B}) \times ran ({A ↾}_{B}) \land dom ({A ↾}_{B}) \times ran ({A ↾}_{B}) \in V) \to {A ↾}_{B} \in V$
12	10 11	mpan	$⊢ dom ({A ↾}_{B}) \times ran ({A ↾}_{B}) \in V \to {A ↾}_{B} \in V$
13	6 7 12	3syl	$⊢ (Fun A \land B \in C) \to {A ↾}_{B} \in V$