Theorem funcnv3

Description: A condition showing a class is single-rooted. (See funcnv ). (Contributed by NM, 26-May-2006)

	Ref	Expression
Assertion	funcnv3	⊢ ( Fun ◡ 𝐴 ↔ ∀ 𝑦 ∈ ran 𝐴 ∃! 𝑥 ∈ dom 𝐴 𝑥 𝐴 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		dfrn2	⊢ ran 𝐴 = { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 }
2	1	abeq2i	⊢ ( 𝑦 ∈ ran 𝐴 ↔ ∃ 𝑥 𝑥 𝐴 𝑦 )
3	2	biimpi	⊢ ( 𝑦 ∈ ran 𝐴 → ∃ 𝑥 𝑥 𝐴 𝑦 )
4	3	biantrurd	⊢ ( 𝑦 ∈ ran 𝐴 → ( ∃* 𝑥 𝑥 𝐴 𝑦 ↔ ( ∃ 𝑥 𝑥 𝐴 𝑦 ∧ ∃* 𝑥 𝑥 𝐴 𝑦 ) ) )
5	4	ralbiia	⊢ ( ∀ 𝑦 ∈ ran 𝐴 ∃* 𝑥 𝑥 𝐴 𝑦 ↔ ∀ 𝑦 ∈ ran 𝐴 ( ∃ 𝑥 𝑥 𝐴 𝑦 ∧ ∃* 𝑥 𝑥 𝐴 𝑦 ) )
6		funcnv	⊢ ( Fun ◡ 𝐴 ↔ ∀ 𝑦 ∈ ran 𝐴 ∃* 𝑥 𝑥 𝐴 𝑦 )
7		df-reu	⊢ ( ∃! 𝑥 ∈ dom 𝐴 𝑥 𝐴 𝑦 ↔ ∃! 𝑥 ( 𝑥 ∈ dom 𝐴 ∧ 𝑥 𝐴 𝑦 ) )
8		vex	⊢ 𝑥 ∈ V
9		vex	⊢ 𝑦 ∈ V
10	8 9	breldm	⊢ ( 𝑥 𝐴 𝑦 → 𝑥 ∈ dom 𝐴 )
11	10	pm4.71ri	⊢ ( 𝑥 𝐴 𝑦 ↔ ( 𝑥 ∈ dom 𝐴 ∧ 𝑥 𝐴 𝑦 ) )
12	11	eubii	⊢ ( ∃! 𝑥 𝑥 𝐴 𝑦 ↔ ∃! 𝑥 ( 𝑥 ∈ dom 𝐴 ∧ 𝑥 𝐴 𝑦 ) )
13		df-eu	⊢ ( ∃! 𝑥 𝑥 𝐴 𝑦 ↔ ( ∃ 𝑥 𝑥 𝐴 𝑦 ∧ ∃* 𝑥 𝑥 𝐴 𝑦 ) )
14	7 12 13	3bitr2i	⊢ ( ∃! 𝑥 ∈ dom 𝐴 𝑥 𝐴 𝑦 ↔ ( ∃ 𝑥 𝑥 𝐴 𝑦 ∧ ∃* 𝑥 𝑥 𝐴 𝑦 ) )
15	14	ralbii	⊢ ( ∀ 𝑦 ∈ ran 𝐴 ∃! 𝑥 ∈ dom 𝐴 𝑥 𝐴 𝑦 ↔ ∀ 𝑦 ∈ ran 𝐴 ( ∃ 𝑥 𝑥 𝐴 𝑦 ∧ ∃* 𝑥 𝑥 𝐴 𝑦 ) )
16	5 6 15	3bitr4i	⊢ ( Fun ◡ 𝐴 ↔ ∀ 𝑦 ∈ ran 𝐴 ∃! 𝑥 ∈ dom 𝐴 𝑥 𝐴 𝑦 )