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