Theorem funmo

Description: A function has at most one value for each argument. (Contributed by NM, 24-May-1998)

	Ref	Expression
Assertion	funmo	⊢ ( Fun 𝐹 → ∃* 𝑦 𝐴 𝐹 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		dffun6	⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 ) )
2	1	simplbi	⊢ ( Fun 𝐹 → Rel 𝐹 )
3		brrelex1	⊢ ( ( Rel 𝐹 ∧ 𝐴 𝐹 𝑦 ) → 𝐴 ∈ V )
4	3	ex	⊢ ( Rel 𝐹 → ( 𝐴 𝐹 𝑦 → 𝐴 ∈ V ) )
5	2 4	syl	⊢ ( Fun 𝐹 → ( 𝐴 𝐹 𝑦 → 𝐴 ∈ V ) )
6	5	ancrd	⊢ ( Fun 𝐹 → ( 𝐴 𝐹 𝑦 → ( 𝐴 ∈ V ∧ 𝐴 𝐹 𝑦 ) ) )
7	6	alrimiv	⊢ ( Fun 𝐹 → ∀ 𝑦 ( 𝐴 𝐹 𝑦 → ( 𝐴 ∈ V ∧ 𝐴 𝐹 𝑦 ) ) )
8		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 𝑦 ↔ 𝐴 𝐹 𝑦 ) )
9	8	mobidv	⊢ ( 𝑥 = 𝐴 → ( ∃* 𝑦 𝑥 𝐹 𝑦 ↔ ∃* 𝑦 𝐴 𝐹 𝑦 ) )
10	9	imbi2d	⊢ ( 𝑥 = 𝐴 → ( ( Fun 𝐹 → ∃* 𝑦 𝑥 𝐹 𝑦 ) ↔ ( Fun 𝐹 → ∃* 𝑦 𝐴 𝐹 𝑦 ) ) )
11	1	simprbi	⊢ ( Fun 𝐹 → ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 )
12	11	19.21bi	⊢ ( Fun 𝐹 → ∃* 𝑦 𝑥 𝐹 𝑦 )
13	10 12	vtoclg	⊢ ( 𝐴 ∈ V → ( Fun 𝐹 → ∃* 𝑦 𝐴 𝐹 𝑦 ) )
14	13	com12	⊢ ( Fun 𝐹 → ( 𝐴 ∈ V → ∃* 𝑦 𝐴 𝐹 𝑦 ) )
15		moanimv	⊢ ( ∃* 𝑦 ( 𝐴 ∈ V ∧ 𝐴 𝐹 𝑦 ) ↔ ( 𝐴 ∈ V → ∃* 𝑦 𝐴 𝐹 𝑦 ) )
16	14 15	sylibr	⊢ ( Fun 𝐹 → ∃* 𝑦 ( 𝐴 ∈ V ∧ 𝐴 𝐹 𝑦 ) )
17		moim	⊢ ( ∀ 𝑦 ( 𝐴 𝐹 𝑦 → ( 𝐴 ∈ V ∧ 𝐴 𝐹 𝑦 ) ) → ( ∃* 𝑦 ( 𝐴 ∈ V ∧ 𝐴 𝐹 𝑦 ) → ∃* 𝑦 𝐴 𝐹 𝑦 ) )
18	7 16 17	sylc	⊢ ( Fun 𝐹 → ∃* 𝑦 𝐴 𝐹 𝑦 )