Theorem ssopab2i

Description: Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995)

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

Proof

Step	Hyp	Ref	Expression
1		ssopab2i.1	$$⊢\phi \to \psi$$
2		ssopab2	$$⊢\forall x\forall y\left(\phi \to \psi \right)\to \left\{⟨x,y⟩|\phi \right\}\subseteq \left\{⟨x,y⟩|\psi \right\}$$
3	1	ax-gen	$$⊢\forall y\left(\phi \to \psi \right)$$
4	2 3	mpg	$$⊢\left\{⟨x,y⟩|\phi \right\}\subseteq \left\{⟨x,y⟩|\psi \right\}$$