Theorem ssopab2bw

Description: Equivalence of ordered pair abstraction subclass and implication. Version of ssopab2b with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 27-Dec-1996) (Revised by Gino Giotto, 26-Jan-2024)

	Ref	Expression
Assertion	ssopab2bw	$$⊢\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		opabidw	$$⊢⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \phi$$
9		opabidw	$$⊢⟨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)$$