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

Metamath Proof Explorer

Theorem opabssxpd

Description: An ordered-pair class abstraction is a subset of a Cartesian product. Formerly part of proof for opabex2 . (Contributed by AV, 26-Nov-2021)

		Ref	Expression
	Hypotheses	opabssxpd.x	$⊢ (φ \land ψ) \to x \in A$
		opabssxpd.y	$⊢ (φ \land ψ) \to y \in B$
	Assertion	opabssxpd	$⊢ φ \to \{⟨x, y⟩ \| ψ\} \subseteq A \times B$

Proof

Step	Hyp	Ref	Expression
1		opabssxpd.x	$⊢ (φ \land ψ) \to x \in A$
2		opabssxpd.y	$⊢ (φ \land ψ) \to y \in B$
3		df-opab	$⊢ \{⟨x, y⟩ \| ψ\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land ψ)\}$
4		simprl	$⊢ (φ \land (z = ⟨x, y⟩ \land ψ)) \to z = ⟨x, y⟩$
5	1 2	opelxpd	$⊢ (φ \land ψ) \to ⟨x, y⟩ \in (A \times B)$
6	5	adantrl	$⊢ (φ \land (z = ⟨x, y⟩ \land ψ)) \to ⟨x, y⟩ \in (A \times B)$
7	4 6	eqeltrd	$⊢ (φ \land (z = ⟨x, y⟩ \land ψ)) \to z \in (A \times B)$
8	7	ex	$⊢ φ \to ((z = ⟨x, y⟩ \land ψ) \to z \in (A \times B))$
9	8	exlimdvv	$⊢ φ \to (\exists x \exists y (z = ⟨x, y⟩ \land ψ) \to z \in (A \times B))$
10	9	abssdv	$⊢ φ \to \{z \| \exists x \exists y (z = ⟨x, y⟩ \land ψ)\} \subseteq A \times B$
11	3 10	eqsstrid	$⊢ φ \to \{⟨x, y⟩ \| ψ\} \subseteq A \times B$