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

Metamath Proof Explorer

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 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∀ 𝑥 ∃* 𝑦 𝜑 )