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	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ψ\} \leftrightarrow \forall x \forall y \forall z (φ \to ψ)$

Proof

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

Metamath Proof Explorer

Theorem ssoprab2b

Proof