Theorem elfunsALTV

Description: Elementhood in the class of functions. (Contributed by Peter Mazsa, 24-Jul-2021)

	Ref	Expression
Assertion	elfunsALTV	⊢ ( 𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels ) )

Proof

Step	Hyp	Ref	Expression
1		dffunsALTV	⊢ FunsALTV = { 𝑥 ∈ Rels ∣ ≀ 𝑥 ∈ CnvRefRels }
2		cosseq	⊢ ( 𝑥 = 𝐹 → ≀ 𝑥 = ≀ 𝐹 )
3	2	eleq1d	⊢ ( 𝑥 = 𝐹 → ( ≀ 𝑥 ∈ CnvRefRels ↔ ≀ 𝐹 ∈ CnvRefRels ) )
4	1 3	rabeqel	⊢ ( 𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels ) )