Metamath Proof Explorer


Theorem dmoprabss

Description: The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995)

Ref Expression
Assertion dmoprabss dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) } ⊆ ( 𝐴 × 𝐵 )

Proof

Step Hyp Ref Expression
1 dmoprab dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) }
2 19.42v ( ∃ 𝑧 ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ∃ 𝑧 𝜑 ) )
3 2 opabbii { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ∃ 𝑧 𝜑 ) }
4 opabssxp { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ∃ 𝑧 𝜑 ) } ⊆ ( 𝐴 × 𝐵 )
5 3 4 eqsstri { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) } ⊆ ( 𝐴 × 𝐵 )
6 1 5 eqsstri dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) } ⊆ ( 𝐴 × 𝐵 )