This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑅 = { 𝑦 ∣ ∃ 𝑥 𝜑 } )