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

Metamath Proof Explorer

Theorem opabex

Description: Existence of a function expressed as class of ordered pairs. (Contributed by NM, 21-Jul-1996)

Ref Expression
Hypotheses opabex.1 ⊢ 𝐴 ∈ V
opabex.2 ⊢ ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝜑 )
Assertion opabex { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∈ V

Proof

Step Hyp Ref Expression
1 opabex.1 ⊢ 𝐴 ∈ V
2 opabex.2 ⊢ ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝜑 )
3 funopab ⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
4 moanimv ⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝜑 ) )
5 2 4 mpbir ⊢ ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
6 3 5 mpgbir ⊢ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
7 dmopabss ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ⊆ 𝐴
8 1 7 ssexi ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∈ V
9 funex ⊢ ( ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∧ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∈ V ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∈ V )
10 6 8 9 mp2an ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∈ V