Theorem ssopab2dv

Description: Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014) (Revised by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypothesis	ssopab2dv.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
Assertion	ssopab2dv	$$⊢\phi \to \left\{⟨x,y⟩|\psi \right\}\subseteq \left\{⟨x,y⟩|\chi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		ssopab2dv.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
2	1	alrimivv	$$⊢\phi \to \forall x\forall y\left(\psi \to \chi \right)$$
3		ssopab2	$$⊢\forall x\forall y\left(\psi \to \chi \right)\to \left\{⟨x,y⟩|\psi \right\}\subseteq \left\{⟨x,y⟩|\chi \right\}$$
4	2 3	syl	$$⊢\phi \to \left\{⟨x,y⟩|\psi \right\}\subseteq \left\{⟨x,y⟩|\chi \right\}$$