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	$$⊢\left(\phi \wedge xW\left(G\right)y\right)\to \psi$$
	opabresex2d.2	$$⊢\phi \to \left\{⟨x,y⟩|\psi \right\}\in V$$
Assertion	opabresex2d	$$⊢\phi \to \left\{⟨x,y⟩|\left(xW\left(G\right)y\wedge \theta \right)\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		opabresex2d.1	$$⊢\left(\phi \wedge xW\left(G\right)y\right)\to \psi$$
2		opabresex2d.2	$$⊢\phi \to \left\{⟨x,y⟩|\psi \right\}\in V$$
3	1	ex	$$⊢\phi \to \left(xW\left(G\right)y\to \psi \right)$$
4	3	alrimivv	$$⊢\phi \to \forall x\forall y\left(xW\left(G\right)y\to \psi \right)$$
5		opabbrex	$$⊢\left(\forall x\forall y\left(xW\left(G\right)y\to \psi \right)\wedge \left\{⟨x,y⟩|\psi \right\}\in V\right)\to \left\{⟨x,y⟩|\left(xW\left(G\right)y\wedge \theta \right)\right\}\in \mathrm{V}$$
6	4 2 5	syl2anc	$$⊢\phi \to \left\{⟨x,y⟩|\left(xW\left(G\right)y\wedge \theta \right)\right\}\in \mathrm{V}$$