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 )