Theorem dffunALTV2

Description: Alternate definition of the function relation predicate, cf. dfdisjALTV2 . (Contributed by Peter Mazsa, 8-Feb-2018)

	Ref	Expression
Assertion	dffunALTV2	⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		df-funALTV	⊢ ( FunALTV 𝐹 ↔ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹 ) )
2		cnvrefrelcoss2	⊢ ( CnvRefRel ≀ 𝐹 ↔ ≀ 𝐹 ⊆ I )
3	2	anbi1i	⊢ ( ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹 ) ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹 ) )
4	1 3	bitri	⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹 ) )