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 φ x W G y ψ
opabresex2d.2 φ x y | ψ V
Assertion opabresex2d φ x y | x W G y θ V

Proof

Step Hyp Ref Expression
1 opabresex2d.1 φ x W G y ψ
2 opabresex2d.2 φ x y | ψ V
3 1 ex φ x W G y ψ
4 3 alrimivv φ x y x W G y ψ
5 opabbrex x y x W G y ψ x y | ψ V x y | x W G y θ V
6 4 2 5 syl2anc φ x y | x W G y θ V