Theorem opabresex2

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) Add disjoint variable conditions betweem W , G and x , y to remove hypotheses. (Revised by SN, 13-Dec-2024)

	Ref	Expression
Assertion	opabresex2	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑊 ‘ 𝐺 ) 𝑦 ∧ 𝜃 ) } ∈ V

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( 𝑊 ‘ 𝐺 ) ∈ V
2		elopabran	⊢ ( 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑊 ‘ 𝐺 ) 𝑦 ∧ 𝜃 ) } → 𝑧 ∈ ( 𝑊 ‘ 𝐺 ) )
3	2	ssriv	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑊 ‘ 𝐺 ) 𝑦 ∧ 𝜃 ) } ⊆ ( 𝑊 ‘ 𝐺 )
4	1 3	ssexi	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝑊 ‘ 𝐺 ) 𝑦 ∧ 𝜃 ) } ∈ V