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	⊢ ( 𝐹 Fn V → ( ◡ 𝐹 “ V ) = V )

Proof

Step	Hyp	Ref	Expression
1		fncnvima2	⊢ ( 𝐹 Fn V → ( ◡ 𝐹 “ V ) = { 𝑦 ∈ V ∣ ( 𝐹 ‘ 𝑦 ) ∈ V } )
2		fveq2	⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
3	2	eleq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑦 ) ∈ V ↔ ( 𝐹 ‘ 𝑥 ) ∈ V ) )
4	3	elrab	⊢ ( 𝑥 ∈ { 𝑦 ∈ V ∣ ( 𝐹 ‘ 𝑦 ) ∈ V } ↔ ( 𝑥 ∈ V ∧ ( 𝐹 ‘ 𝑥 ) ∈ V ) )
5		fvexd	⊢ ( 𝐹 Fn V → ( 𝐹 ‘ 𝑥 ) ∈ V )
6	5	biantrud	⊢ ( 𝐹 Fn V → ( 𝑥 ∈ V ↔ ( 𝑥 ∈ V ∧ ( 𝐹 ‘ 𝑥 ) ∈ V ) ) )
7	4 6	bitr4id	⊢ ( 𝐹 Fn V → ( 𝑥 ∈ { 𝑦 ∈ V ∣ ( 𝐹 ‘ 𝑦 ) ∈ V } ↔ 𝑥 ∈ V ) )
8	7	eqrdv	⊢ ( 𝐹 Fn V → { 𝑦 ∈ V ∣ ( 𝐹 ‘ 𝑦 ) ∈ V } = V )
9	1 8	eqtrd	⊢ ( 𝐹 Fn V → ( ◡ 𝐹 “ V ) = V )