Theorem dmopab

Description: The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995) (Revised by Mario Carneiro, 4-Dec-2016)

	Ref	Expression
Assertion	dmopab	⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑥 ∣ ∃ 𝑦 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		nfopab1	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2		nfopab2	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
3	1 2	dfdmf	⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑥 ∣ ∃ 𝑦 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 }
4		df-br	⊢ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
5		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜑 )
6	4 5	bitri	⊢ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ↔ 𝜑 )
7	6	exbii	⊢ ( ∃ 𝑦 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ↔ ∃ 𝑦 𝜑 )
8	7	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 } = { 𝑥 ∣ ∃ 𝑦 𝜑 }
9	3 8	eqtri	⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑥 ∣ ∃ 𝑦 𝜑 }