Theorem funcnv2

Description: A simpler equivalence for single-rooted (see funcnv ). (Contributed by NM, 9-Aug-2004)

	Ref	Expression
Assertion	funcnv2	⊢ ( Fun ◡ 𝐴 ↔ ∀ 𝑦 ∃* 𝑥 𝑥 𝐴 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		relcnv	⊢ Rel ◡ 𝐴
2		dffun6	⊢ ( Fun ◡ 𝐴 ↔ ( Rel ◡ 𝐴 ∧ ∀ 𝑦 ∃* 𝑥 𝑦 ◡ 𝐴 𝑥 ) )
3	1 2	mpbiran	⊢ ( Fun ◡ 𝐴 ↔ ∀ 𝑦 ∃* 𝑥 𝑦 ◡ 𝐴 𝑥 )
4		vex	⊢ 𝑦 ∈ V
5		vex	⊢ 𝑥 ∈ V
6	4 5	brcnv	⊢ ( 𝑦 ◡ 𝐴 𝑥 ↔ 𝑥 𝐴 𝑦 )
7	6	mobii	⊢ ( ∃* 𝑥 𝑦 ◡ 𝐴 𝑥 ↔ ∃* 𝑥 𝑥 𝐴 𝑦 )
8	7	albii	⊢ ( ∀ 𝑦 ∃* 𝑥 𝑦 ◡ 𝐴 𝑥 ↔ ∀ 𝑦 ∃* 𝑥 𝑥 𝐴 𝑦 )
9	3 8	bitri	⊢ ( Fun ◡ 𝐴 ↔ ∀ 𝑦 ∃* 𝑥 𝑥 𝐴 𝑦 )