Theorem rnopab

Description: The range of a class of ordered pairs. (Contributed by NM, 14-Aug-1995) (Revised by Mario Carneiro, 4-Dec-2016)

	Ref	Expression
Assertion	rnopab	⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑦 ∣ ∃ 𝑥 𝜑 }

Proof

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