Metamath Proof Explorer

Theorem ssopab2

Description: Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996) (Revised by Mario Carneiro, 19-May-2013)

		Ref	Expression
	Assertion	ssopab2	$⊢ \forall x \forall y (φ \to ψ) \to \{⟨x, y⟩ \| φ\} \subseteq \{⟨x, y⟩ \| ψ\}$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ (φ \to ψ) \to (φ \to ψ)$
2	1	anim2d	$⊢ (φ \to ψ) \to ((z = ⟨x, y⟩ \land φ) \to (z = ⟨x, y⟩ \land ψ))$
3	2	aleximi	$⊢ \forall y (φ \to ψ) \to (\exists y (z = ⟨x, y⟩ \land φ) \to \exists y (z = ⟨x, y⟩ \land ψ))$
4	3	aleximi	$⊢ \forall x \forall y (φ \to ψ) \to (\exists x \exists y (z = ⟨x, y⟩ \land φ) \to \exists x \exists y (z = ⟨x, y⟩ \land ψ))$
5	4	ss2abdv	$⊢ \forall x \forall y (φ \to ψ) \to \{z \| \exists x \exists y (z = ⟨x, y⟩ \land φ)\} \subseteq \{z \| \exists x \exists y (z = ⟨x, y⟩ \land ψ)\}$
6		df-opab	$⊢ \{⟨x, y⟩ \| φ\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land φ)\}$
7		df-opab	$⊢ \{⟨x, y⟩ \| ψ\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land ψ)\}$
8	5 6 7	3sstr4g	$⊢ \forall x \forall y (φ \to ψ) \to \{⟨x, y⟩ \| φ\} \subseteq \{⟨x, y⟩ \| ψ\}$