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 ranE-1A=A

Proof

Step Hyp Ref Expression
1 rnopab ranxy|xAyx=y|xxAyx
2 cnvepres E-1A=xy|xAyx
3 2 rneqi ranE-1A=ranxy|xAyx
4 dfuni2 A=y|xAyx
5 df-rex xAyxxxAyx
6 5 abbii y|xAyx=y|xxAyx
7 4 6 eqtri A=y|xxAyx
8 1 3 7 3eqtr4i ranE-1A=A