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	$$⊢{\mathrm{Base}}^{-1}\left[\mathrm{V}\right]=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		basfn	$$⊢\mathrm{Base}Fn\mathrm{V}$$
2		fncnvimaeqv	$$⊢\mathrm{Base}Fn\mathrm{V}\to {\mathrm{Base}}^{-1}\left[\mathrm{V}\right]=\mathrm{V}$$
3	1 2	ax-mp	$$⊢{\mathrm{Base}}^{-1}\left[\mathrm{V}\right]=\mathrm{V}$$