Metamath Proof Explorer


Theorem opabdm

Description: Domain of an ordered-pair class abstraction. (Contributed by Thierry Arnoux, 31-Aug-2017)

Ref Expression
Assertion opabdm ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → dom 𝑅 = { 𝑥 ∣ ∃ 𝑦 𝜑 } )

Proof

Step Hyp Ref Expression
1 df-dm dom 𝑅 = { 𝑥 ∣ ∃ 𝑦 𝑥 𝑅 𝑦 }
2 nfopab1 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
3 2 nfeq2 𝑥 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
4 nfopab2 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
5 4 nfeq2 𝑦 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
6 df-br ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
7 eleq2 ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) )
8 opabidw ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜑 )
9 7 8 bitrdi ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅𝜑 ) )
10 6 9 syl5bb ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ( 𝑥 𝑅 𝑦𝜑 ) )
11 5 10 exbid ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ( ∃ 𝑦 𝑥 𝑅 𝑦 ↔ ∃ 𝑦 𝜑 ) )
12 3 11 abbid ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → { 𝑥 ∣ ∃ 𝑦 𝑥 𝑅 𝑦 } = { 𝑥 ∣ ∃ 𝑦 𝜑 } )
13 1 12 syl5eq ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → dom 𝑅 = { 𝑥 ∣ ∃ 𝑦 𝜑 } )