Theorem dffunsALTV

Description: Alternate definition of the class of functions. (Contributed by Peter Mazsa, 18-Jul-2021)

	Ref	Expression
Assertion	dffunsALTV	⊢ FunsALTV = { 𝑓 ∈ Rels ∣ ≀ 𝑓 ∈ CnvRefRels }

Proof

Step	Hyp	Ref	Expression
1		df-funsALTV	⊢ FunsALTV = ( Funss ∩ Rels )
2		df-funss	⊢ Funss = { 𝑓 ∣ ≀ 𝑓 ∈ CnvRefRels }
3	1 2	abeqin	⊢ FunsALTV = { 𝑓 ∈ Rels ∣ ≀ 𝑓 ∈ CnvRefRels }