This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssoprab2

Description: Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 . (Contributed by FL, 6-Nov-2013) (Proof shortened by Mario Carneiro, 11-Dec-2016)

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

Proof

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