funimaexg

Description: Axiom of Replacement using abbreviations. Axiom 39(vi) of Quine p. 284. Compare Exercise 9 of TakeutiZaring p. 29. (Contributed by NM, 10-Sep-2006) Shorten proof and avoid ax-10 , ax-12 . (Revised by SN, 19-Dec-2024)

		Ref	Expression
	Assertion	funimaexg	$⊢ (Fun A \land B \in C) \to A [B] \in V$

Proof

Step	Hyp	Ref	Expression
1		dffun6	$⊢ Fun A \leftrightarrow (Rel A \land \forall x \exists^{*} y x A y)$
2	1	simprbi	$⊢ Fun A \to \forall x \exists^{*} y x A y$
3		dfima2	$⊢ A [B] = \{y \| \exists x \in B x A y\}$
4		axrep6g	$⊢ (B \in C \land \forall x \exists^{*} y x A y) \to \{y \| \exists x \in B x A y\} \in V$
5	3 4	eqeltrid	$⊢ (B \in C \land \forall x \exists^{*} y x A y) \to A [B] \in V$
6	2 5	sylan2	$⊢ (B \in C \land Fun A) \to A [B] \in V$
7	6	ancoms	$⊢ (Fun A \land B \in C) \to A [B] \in V$

Metamath Proof Explorer

Theorem funimaexg

Proof