Theorem ssopab2b

Description: Equivalence of ordered pair abstraction subclass and implication. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker ssopab2bw when possible. (Contributed by NM, 27-Dec-1996) (Proof shortened by Mario Carneiro, 18-Nov-2016) (New usage is discouraged.)

	Ref	Expression
Assertion	ssopab2b	$$⊢\left\{⟨x,y⟩|\phi \right\}\subseteq \left\{⟨x,y⟩|\psi \right\}\leftrightarrow \forall x\forall y\left(\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfopab1	$$⊢\underset{\_}{Ⅎ}x\left\{⟨x,y⟩|\phi \right\}$$
2		nfopab1	$$⊢\underset{\_}{Ⅎ}x\left\{⟨x,y⟩|\psi \right\}$$
3	1 2	nfss	$$⊢Ⅎx\left\{⟨x,y⟩|\phi \right\}\subseteq \left\{⟨x,y⟩|\psi \right\}$$
4		nfopab2	$$⊢\underset{\_}{Ⅎ}y\left\{⟨x,y⟩|\phi \right\}$$
5		nfopab2	$$⊢\underset{\_}{Ⅎ}y\left\{⟨x,y⟩|\psi \right\}$$
6	4 5	nfss	$$⊢Ⅎy\left\{⟨x,y⟩|\phi \right\}\subseteq \left\{⟨x,y⟩|\psi \right\}$$
7		ssel	$$⊢\left\{⟨x,y⟩|\phi \right\}\subseteq \left\{⟨x,y⟩|\psi \right\}\to \left(⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\to ⟨x,y⟩\in \left\{⟨x,y⟩|\psi \right\}\right)$$
8		opabid	$$⊢⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \phi$$
9		opabid	$$⊢⟨x,y⟩\in \left\{⟨x,y⟩|\psi \right\}\leftrightarrow \psi$$
10	7 8 9	3imtr3g	$$⊢\left\{⟨x,y⟩|\phi \right\}\subseteq \left\{⟨x,y⟩|\psi \right\}\to \left(\phi \to \psi \right)$$
11	6 10	alrimi	$$⊢\left\{⟨x,y⟩|\phi \right\}\subseteq \left\{⟨x,y⟩|\psi \right\}\to \forall y\left(\phi \to \psi \right)$$
12	3 11	alrimi	$$⊢\left\{⟨x,y⟩|\phi \right\}\subseteq \left\{⟨x,y⟩|\psi \right\}\to \forall x\forall y\left(\phi \to \psi \right)$$
13		ssopab2	$$⊢\forall x\forall y\left(\phi \to \psi \right)\to \left\{⟨x,y⟩|\phi \right\}\subseteq \left\{⟨x,y⟩|\psi \right\}$$
14	12 13	impbii	$$⊢\left\{⟨x,y⟩|\phi \right\}\subseteq \left\{⟨x,y⟩|\psi \right\}\leftrightarrow \forall x\forall y\left(\phi \to \psi \right)$$