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	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑥 ∈ 𝐴 )
		opabssxpd.y	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑦 ∈ 𝐵 )
	Assertion	opabssxpd	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ⊆ ( 𝐴 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		opabssxpd.x	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑥 ∈ 𝐴 )
2		opabssxpd.y	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑦 ∈ 𝐵 )
3		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) }
4		simprl	⊢ ( ( 𝜑 ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) → 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
5	1 2	opelxpd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) )
6	5	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) )
7	4 6	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) → 𝑧 ∈ ( 𝐴 × 𝐵 ) )
8	7	ex	⊢ ( 𝜑 → ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) → 𝑧 ∈ ( 𝐴 × 𝐵 ) ) )
9	8	exlimdvv	⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) → 𝑧 ∈ ( 𝐴 × 𝐵 ) ) )
10	9	abssdv	⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) } ⊆ ( 𝐴 × 𝐵 ) )
11	3 10	eqsstrid	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ⊆ ( 𝐴 × 𝐵 ) )