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

Proof

Step	Hyp	Ref	Expression
1		fncnvima2	$$⊢FFn\mathrm{V}\to F^{-1}\left[\mathrm{V}\right]=\left\{y\in \mathrm{V}|F\left(y\right)\in \mathrm{V}\right\}$$
2		fveq2	$$⊢y=x\to F\left(y\right)=F\left(x\right)$$
3	2	eleq1d	$$⊢y=x\to \left(F\left(y\right)\in \mathrm{V}\leftrightarrow F\left(x\right)\in \mathrm{V}\right)$$
4	3	elrab	$$⊢x\in \left\{y\in \mathrm{V}|F\left(y\right)\in \mathrm{V}\right\}\leftrightarrow \left(x\in \mathrm{V}\wedge F\left(x\right)\in \mathrm{V}\right)$$
5		fvexd	$$⊢FFn\mathrm{V}\to F\left(x\right)\in \mathrm{V}$$
6	5	biantrud	$$⊢FFn\mathrm{V}\to \left(x\in \mathrm{V}\leftrightarrow \left(x\in \mathrm{V}\wedge F\left(x\right)\in \mathrm{V}\right)\right)$$
7	4 6	bitr4id	$$⊢FFn\mathrm{V}\to \left(x\in \left\{y\in \mathrm{V}|F\left(y\right)\in \mathrm{V}\right\}\leftrightarrow x\in \mathrm{V}\right)$$
8	7	eqrdv	$$⊢FFn\mathrm{V}\to \left\{y\in \mathrm{V}|F\left(y\right)\in \mathrm{V}\right\}=\mathrm{V}$$
9	1 8	eqtrd	$$⊢FFn\mathrm{V}\to F^{-1}\left[\mathrm{V}\right]=\mathrm{V}$$