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

Proof

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

Metamath Proof Explorer

Theorem fncnvimaeqv

Proof