Metamath Proof Explorer


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 x y | x W G y θ V

Proof

Step Hyp Ref Expression
1 fvex W G V
2 elopabran z x y | x W G y θ z W G
3 2 ssriv x y | x W G y θ W G
4 1 3 ssexi x y | x W G y θ V