Theorem rnoprab

Description: The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004) (Revised by David Abernethy, 19-Apr-2013)

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

Proof

Step	Hyp	Ref	Expression
1		dfoprab2	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
2	1	rneqi	⊢ ran { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = ran { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
3		rnopab	⊢ ran { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
4		exrot3	⊢ ( ∃ 𝑤 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑤 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
5		opex	⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
6	5	isseti	⊢ ∃ 𝑤 𝑤 = ⟨ 𝑥 , 𝑦 ⟩
7		19.41v	⊢ ( ∃ 𝑤 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ∃ 𝑤 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
8	6 7	mpbiran	⊢ ( ∃ 𝑤 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ 𝜑 )
9	8	2exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑤 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 𝜑 )
10	4 9	bitri	⊢ ( ∃ 𝑤 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 𝜑 )
11	10	abbii	⊢ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 𝜑 }
12	2 3 11	3eqtri	⊢ ran { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 𝜑 }