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	bitrid	⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ( 𝑥 𝑅 𝑦 ↔ 𝜑 ) )
11	5 10	exbid	⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ( ∃ 𝑦 𝑥 𝑅 𝑦 ↔ ∃ 𝑦 𝜑 ) )
12	3 11	abbid	⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → { 𝑥 ∣ ∃ 𝑦 𝑥 𝑅 𝑦 } = { 𝑥 ∣ ∃ 𝑦 𝜑 } )
13	1 12	eqtrid	⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → dom 𝑅 = { 𝑥 ∣ ∃ 𝑦 𝜑 } )