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

Metamath Proof Explorer

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 |` A ) = U. A

Proof

Step Hyp Ref Expression
1 rnopab 
 |-  ran { <. x , y >. | ( x e. A /\ y e. x ) } = { y | E. x ( x e. A /\ y e. x ) }
2 cnvepres 
 |-  ( `' _E |` A ) = { <. x , y >. | ( x e. A /\ y e. x ) }
3 2 rneqi 
 |-  ran ( `' _E |` A ) = ran { <. x , y >. | ( x e. A /\ y e. x ) }
4 dfuni2 
 |-  U. A = { y | E. x e. A y e. x }
5 df-rex 
 |-  ( E. x e. A y e. x <-> E. x ( x e. A /\ y e. x ) )
6 5 abbii 
 |-  { y | E. x e. A y e. x } = { y | E. x ( x e. A /\ y e. x ) }
7 4 6 eqtri 
 |-  U. A = { y | E. x ( x e. A /\ y e. x ) }
8 1 3 7 3eqtr4i 
 |-  ran ( `' _E |` A ) = U. A