Metamath Proof Explorer


Theorem opabresex2d

Description: Restrictions of a collection of ordered pairs of related elements are sets. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 15-Jan-2021)

Ref Expression
Hypotheses opabresex2d.1 ( ( 𝜑𝑥 ( 𝑊𝐺 ) 𝑦 ) → 𝜓 )
opabresex2d.2 ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∈ 𝑉 )
Assertion opabresex2d ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑊𝐺 ) 𝑦𝜃 ) } ∈ V )

Proof

Step Hyp Ref Expression
1 opabresex2d.1 ( ( 𝜑𝑥 ( 𝑊𝐺 ) 𝑦 ) → 𝜓 )
2 opabresex2d.2 ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∈ 𝑉 )
3 1 ex ( 𝜑 → ( 𝑥 ( 𝑊𝐺 ) 𝑦𝜓 ) )
4 3 alrimivv ( 𝜑 → ∀ 𝑥𝑦 ( 𝑥 ( 𝑊𝐺 ) 𝑦𝜓 ) )
5 opabbrex ( ( ∀ 𝑥𝑦 ( 𝑥 ( 𝑊𝐺 ) 𝑦𝜓 ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∈ 𝑉 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑊𝐺 ) 𝑦𝜃 ) } ∈ V )
6 4 2 5 syl2anc ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑊𝐺 ) 𝑦𝜃 ) } ∈ V )