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 ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ⊆ ( 𝐴 × 𝐵 ) )