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