Theorem dffun9

Description: Alternate definition of a function. (Contributed by NM, 28-Mar-2007) (Revised by NM, 16-Jun-2017)

	Ref	Expression
Assertion	dffun9	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 ∈ ran 𝐴 𝑥 𝐴 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		dffun7	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 𝑥 𝐴 𝑦 ) )
2		vex	⊢ 𝑥 ∈ V
3		vex	⊢ 𝑦 ∈ V
4	2 3	brelrn	⊢ ( 𝑥 𝐴 𝑦 → 𝑦 ∈ ran 𝐴 )
5	4	pm4.71ri	⊢ ( 𝑥 𝐴 𝑦 ↔ ( 𝑦 ∈ ran 𝐴 ∧ 𝑥 𝐴 𝑦 ) )
6	5	mobii	⊢ ( ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∃* 𝑦 ( 𝑦 ∈ ran 𝐴 ∧ 𝑥 𝐴 𝑦 ) )
7		df-rmo	⊢ ( ∃* 𝑦 ∈ ran 𝐴 𝑥 𝐴 𝑦 ↔ ∃* 𝑦 ( 𝑦 ∈ ran 𝐴 ∧ 𝑥 𝐴 𝑦 ) )
8	6 7	bitr4i	⊢ ( ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∃* 𝑦 ∈ ran 𝐴 𝑥 𝐴 𝑦 )
9	8	ralbii	⊢ ( ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 ∈ ran 𝐴 𝑥 𝐴 𝑦 )
10	9	anbi2i	⊢ ( ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 𝑥 𝐴 𝑦 ) ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 ∈ ran 𝐴 𝑥 𝐴 𝑦 ) )
11	1 10	bitri	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∃* 𝑦 ∈ ran 𝐴 𝑥 𝐴 𝑦 ) )