Theorem rncnvepres

Description: The range of the restricted converse epsilon is the union of the restriction. (Contributed by Peter Mazsa, 11-Feb-2018) (Revised by Peter Mazsa, 26-Sep-2021)

	Ref	Expression
Assertion	rncnvepres	⊢ ran ( ◡ E ↾ 𝐴 ) = ∪ 𝐴

Proof

Step	Hyp	Ref	Expression
1		rnopab	⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) }
2		cnvepres	⊢ ( ◡ E ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) }
3	2	rneqi	⊢ ran ( ◡ E ↾ 𝐴 ) = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) }
4		dfuni2	⊢ ∪ 𝐴 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 }
5		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
6	5	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) }
7	4 6	eqtri	⊢ ∪ 𝐴 = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) }
8	1 3 7	3eqtr4i	⊢ ran ( ◡ E ↾ 𝐴 ) = ∪ 𝐴