Theorem funopab

Description: A class of ordered pairs is a function when there is at most one second member for each pair. (Contributed by NM, 16-May-1995)

	Ref	Expression
Assertion	funopab	⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∀ 𝑥 ∃* 𝑦 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		relopabv	⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2		nfopab1	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
3		nfopab2	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
4	2 3	dffun6f	⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ( Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ ∀ 𝑥 ∃* 𝑦 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ) )
5	1 4	mpbiran	⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∀ 𝑥 ∃* 𝑦 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 )
6		df-br	⊢ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
7		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜑 )
8	6 7	bitri	⊢ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ↔ 𝜑 )
9	8	mobii	⊢ ( ∃* 𝑦 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ↔ ∃* 𝑦 𝜑 )
10	9	albii	⊢ ( ∀ 𝑥 ∃* 𝑦 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ↔ ∀ 𝑥 ∃* 𝑦 𝜑 )
11	5 10	bitri	⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∀ 𝑥 ∃* 𝑦 𝜑 )