Theorem svrelfun

Description: A single-valued relation is a function. (See fun2cnv for "single-valued.") Definition 6.4(4) of TakeutiZaring p. 24. (Contributed by NM, 17-Jan-2006)

	Ref	Expression
Assertion	svrelfun	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ Fun ◡ ◡ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		dffun6	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) )
2		fun2cnv	⊢ ( Fun ◡ ◡ 𝐴 ↔ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 )
3	2	anbi2i	⊢ ( ( Rel 𝐴 ∧ Fun ◡ ◡ 𝐴 ) ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) )
4	1 3	bitr4i	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ Fun ◡ ◡ 𝐴 ) )