Metamath Proof Explorer

Theorem funmoOLD

Description: Obsolete version of funmo as of 19-Dec-2024. (Contributed by NM, 24-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	funmoOLD	$⊢ Fun F \to \exists^{*} y A F y$

Proof

Step	Hyp	Ref	Expression
1		dffun6	$⊢ Fun F \leftrightarrow (Rel F \land \forall x \exists^{*} y x F y)$
2	1	simplbi	$⊢ Fun F \to Rel F$
3		brrelex1	$⊢ (Rel F \land A F y) \to A \in V$
4	3	ex	$⊢ Rel F \to (A F y \to A \in V)$
5	2 4	syl	$⊢ Fun F \to (A F y \to A \in V)$
6	5	ancrd	$⊢ Fun F \to (A F y \to (A \in V \land A F y))$
7	6	alrimiv	$⊢ Fun F \to \forall y (A F y \to (A \in V \land A F y))$
8		breq1	$⊢ x = A \to (x F y \leftrightarrow A F y)$
9	8	mobidv	$⊢ x = A \to (\exists^{} y x F y \leftrightarrow \exists^{} y A F y)$
10	9	imbi2d	$⊢ x = A \to ((Fun F \to \exists^{} y x F y) \leftrightarrow (Fun F \to \exists^{} y A F y))$
11	1	simprbi	$⊢ Fun F \to \forall x \exists^{*} y x F y$
12	11	19.21bi	$⊢ Fun F \to \exists^{*} y x F y$
13	10 12	vtoclg	$⊢ A \in V \to (Fun F \to \exists^{*} y A F y)$
14	13	com12	$⊢ Fun F \to (A \in V \to \exists^{*} y A F y)$
15		moanimv	$⊢ \exists^{} y (A \in V \land A F y) \leftrightarrow (A \in V \to \exists^{} y A F y)$
16	14 15	sylibr	$⊢ Fun F \to \exists^{*} y (A \in V \land A F y)$
17		moim	$⊢ \forall y (A F y \to (A \in V \land A F y)) \to (\exists^{} y (A \in V \land A F y) \to \exists^{} y A F y)$
18	7 16 17	sylc	$⊢ Fun F \to \exists^{*} y A F y$