Theorem ssoprab2b

Description: Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by FL, 6-Nov-2013) (Proof shortened by Mario Carneiro, 11-Dec-2016) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nfoprab1	$$⊢\underset{\_}{Ⅎ}x\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
2		nfoprab1	$$⊢\underset{\_}{Ⅎ}x\left\{⟨⟨x,y⟩,z⟩|\psi \right\}$$
3	1 2	nfss	$$⊢Ⅎx\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \left\{⟨⟨x,y⟩,z⟩|\psi \right\}$$
4		nfoprab2	$$⊢\underset{\_}{Ⅎ}y\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
5		nfoprab2	$$⊢\underset{\_}{Ⅎ}y\left\{⟨⟨x,y⟩,z⟩|\psi \right\}$$
6	4 5	nfss	$$⊢Ⅎy\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \left\{⟨⟨x,y⟩,z⟩|\psi \right\}$$
7		nfoprab3	$$⊢\underset{\_}{Ⅎ}z\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
8		nfoprab3	$$⊢\underset{\_}{Ⅎ}z\left\{⟨⟨x,y⟩,z⟩|\psi \right\}$$
9	7 8	nfss	$$⊢Ⅎz\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \left\{⟨⟨x,y⟩,z⟩|\psi \right\}$$
10		ssel	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \left\{⟨⟨x,y⟩,z⟩|\psi \right\}\to \left(⟨⟨x,y⟩,z⟩\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\to ⟨⟨x,y⟩,z⟩\in \left\{⟨⟨x,y⟩,z⟩|\psi \right\}\right)$$
11		oprabid	$$⊢⟨⟨x,y⟩,z⟩\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\leftrightarrow \phi$$
12		oprabid	$$⊢⟨⟨x,y⟩,z⟩\in \left\{⟨⟨x,y⟩,z⟩|\psi \right\}\leftrightarrow \psi$$
13	10 11 12	3imtr3g	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \left\{⟨⟨x,y⟩,z⟩|\psi \right\}\to \left(\phi \to \psi \right)$$
14	9 13	alrimi	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \left\{⟨⟨x,y⟩,z⟩|\psi \right\}\to \forall z\left(\phi \to \psi \right)$$
15	6 14	alrimi	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \left\{⟨⟨x,y⟩,z⟩|\psi \right\}\to \forall y\forall z\left(\phi \to \psi \right)$$
16	3 15	alrimi	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \left\{⟨⟨x,y⟩,z⟩|\psi \right\}\to \forall x\forall y\forall z\left(\phi \to \psi \right)$$
17		ssoprab2	$$⊢\forall x\forall y\forall z\left(\phi \to \psi \right)\to \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \left\{⟨⟨x,y⟩,z⟩|\psi \right\}$$
18	16 17	impbii	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}\subseteq \left\{⟨⟨x,y⟩,z⟩|\psi \right\}\leftrightarrow \forall x\forall y\forall z\left(\phi \to \psi \right)$$