Theorem bascnvimaeqv

Description: The inverse image of the universal class _V under the base function is the universal class _V itself. (Proposed by Mario Carneiro, 7-Mar-2020.) (Contributed by AV, 7-Mar-2020)

	Ref	Expression
Assertion	bascnvimaeqv	|- ( `' Base " _V ) = _V

Proof

Step	Hyp	Ref	Expression
1		basfn	|- Base Fn _V
2		fncnvimaeqv	|- ( Base Fn _V -> ( `' Base " _V ) = _V )
3	1 2	ax-mp	|- ( `' Base " _V ) = _V