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

Metamath Proof Explorer

Theorem ssoprab2i

Description: Inference of operation class abstraction subclass from implication. (Contributed by NM, 11-Nov-1995) (Revised by David Abernethy, 19-Jun-2012)

		Ref	Expression
	Hypothesis	ssoprab2i.1	$⊢ φ \to ψ$
	Assertion	ssoprab2i	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ψ\}$

Proof

Step	Hyp	Ref	Expression
1		ssoprab2i.1	$⊢ φ \to ψ$
2	1	anim2i	$⊢ (w = ⟨x, y⟩ \land φ) \to (w = ⟨x, y⟩ \land ψ)$
3	2	2eximi	$⊢ \exists x \exists y (w = ⟨x, y⟩ \land φ) \to \exists x \exists y (w = ⟨x, y⟩ \land ψ)$
4	3	ssopab2i	$⊢ \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} \subseteq \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land ψ)\}$
5		dfoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
6		dfoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| ψ\} = \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land ψ)\}$
7	4 5 6	3sstr4i	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ψ\}$