Theorem fncnvimaeqv

Description: The inverse images of the universal class _V under functions on the universal class _V are the universal class _V itself. (Proposed by Mario Carneiro, 7-Mar-2020.) (Contributed by AV, 7-Mar-2020)

	Ref	Expression
Assertion	fncnvimaeqv	|- ( F Fn _V -> ( `' F " _V ) = _V )

Proof

Step	Hyp	Ref	Expression
1		fncnvima2	|- ( F Fn _V -> ( `' F " _V ) = { y e. _V | ( F ` y ) e. _V } )
2		fveq2	|- ( y = x -> ( F ` y ) = ( F ` x ) )
3	2	eleq1d	|- ( y = x -> ( ( F ` y ) e. _V <-> ( F ` x ) e. _V ) )
4	3	elrab	|- ( x e. { y e. _V | ( F ` y ) e. _V } <-> ( x e. _V /\ ( F ` x ) e. _V ) )
5		fvexd	|- ( F Fn _V -> ( F ` x ) e. _V )
6	5	biantrud	|- ( F Fn _V -> ( x e. _V <-> ( x e. _V /\ ( F ` x ) e. _V ) ) )
7	4 6	bitr4id	|- ( F Fn _V -> ( x e. { y e. _V | ( F ` y ) e. _V } <-> x e. _V ) )
8	7	eqrdv	|- ( F Fn _V -> { y e. _V | ( F ` y ) e. _V } = _V )
9	1 8	eqtrd	|- ( F Fn _V -> ( `' F " _V ) = _V )