Theorem opabex2

Description: Condition for an operation to be a set. (Contributed by Thierry Arnoux, 25-Jun-2019)

	Ref	Expression
Hypotheses	opabex2.1	$$⊢\phi \to A\in V$$
	opabex2.2	$$⊢\phi \to B\in W$$
	opabex2.3	$$⊢\left(\phi \wedge \psi \right)\to x\in A$$
	opabex2.4	$$⊢\left(\phi \wedge \psi \right)\to y\in B$$
Assertion	opabex2	$$⊢\phi \to \left\{⟨x,y⟩|\psi \right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		opabex2.1	$$⊢\phi \to A\in V$$
2		opabex2.2	$$⊢\phi \to B\in W$$
3		opabex2.3	$$⊢\left(\phi \wedge \psi \right)\to x\in A$$
4		opabex2.4	$$⊢\left(\phi \wedge \psi \right)\to y\in B$$
5	1 2	xpexd	$$⊢\phi \to A\times B\in \mathrm{V}$$
6	3 4	opabssxpd	$$⊢\phi \to \left\{⟨x,y⟩|\psi \right\}\subseteq A\times B$$
7	5 6	ssexd	$$⊢\phi \to \left\{⟨x,y⟩|\psi \right\}\in \mathrm{V}$$