Theorem opabrn

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

	Ref	Expression
Assertion	opabrn	⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ran 𝑅 = { 𝑦 ∣ ∃ 𝑥 𝜑 } )

Proof

Step	Hyp	Ref	Expression
1		dfrn2	⊢ ran 𝑅 = { 𝑦 ∣ ∃ 𝑥 𝑥 𝑅 𝑦 }
2		nfopab2	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
3	2	nfeq2	⊢ Ⅎ 𝑦 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
4		nfopab1	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
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	⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ran 𝑅 = { 𝑦 ∣ ∃ 𝑥 𝜑 } )