Metamath Proof Explorer

Theorem opabresex2d

Description: Obsolete version of opabresex2 as of 13-Dec-2024. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 15-Jan-2021) (Proof modification is discouraged.) (New usage is discouraged.)

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