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 -1 V = V

Proof

Step Hyp Ref Expression
1 fncnvima2 F Fn V F -1 V = y V | F y V
2 fveq2 y = x F y = F x
3 2 eleq1d y = x F y V F x V
4 3 elrab x y V | F y V x V F x V
5 fvexd F Fn V F x V
6 5 biantrud F Fn V x V x V F x V
7 4 6 bitr4id F Fn V x y V | F y V x V
8 7 eqrdv F Fn V y V | F y V = V
9 1 8 eqtrd F Fn V F -1 V = V