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