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

Metamath Proof Explorer

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 )