This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elfunsALTVfunALTV

Description: The element of the class of functions and the function predicate are the same when F is a set. (Contributed by Peter Mazsa, 26-Jul-2021)

		Ref	Expression
	Assertion	elfunsALTVfunALTV	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ FunsALTV ↔ FunALTV 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		cossex	⊢ ( 𝐹 ∈ 𝑉 → ≀ 𝐹 ∈ V )
2		elcnvrefrelsrel	⊢ ( ≀ 𝐹 ∈ V → ( ≀ 𝐹 ∈ CnvRefRels ↔ CnvRefRel ≀ 𝐹 ) )
3	1 2	syl	⊢ ( 𝐹 ∈ 𝑉 → ( ≀ 𝐹 ∈ CnvRefRels ↔ CnvRefRel ≀ 𝐹 ) )
4		elrelsrel	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ Rels ↔ Rel 𝐹 ) )
5	3 4	anbi12d	⊢ ( 𝐹 ∈ 𝑉 → ( ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels ) ↔ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹 ) ) )
6		elfunsALTV	⊢ ( 𝐹 ∈ FunsALTV ↔ ( ≀ 𝐹 ∈ CnvRefRels ∧ 𝐹 ∈ Rels ) )
7		df-funALTV	⊢ ( FunALTV 𝐹 ↔ ( CnvRefRel ≀ 𝐹 ∧ Rel 𝐹 ) )
8	5 6 7	3bitr4g	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ FunsALTV ↔ FunALTV 𝐹 ) )