Theorem fveqvfvv

Description: If a function's value at an argument is the universal class (which can never be the case because of fvex ), the function's value at this argument is any set (especially the empty set). In short "If a function's value is a proper class, it is a set", which sounds strange/contradictory, but which is a consequence of that a contradiction implies anything (see pm2.21i ). (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Assertion	fveqvfvv	⊢ ( ( 𝐹 ‘ 𝐴 ) = V → ( 𝐹 ‘ 𝐴 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
2		eleq1a	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ V → ( V = ( 𝐹 ‘ 𝐴 ) → V ∈ V ) )
3	1 2	ax-mp	⊢ ( V = ( 𝐹 ‘ 𝐴 ) → V ∈ V )
4		vprc	⊢ ¬ V ∈ V
5	4	pm2.21i	⊢ ( V ∈ V → ( 𝐹 ‘ 𝐴 ) = 𝐵 )
6	3 5	syl	⊢ ( V = ( 𝐹 ‘ 𝐴 ) → ( 𝐹 ‘ 𝐴 ) = 𝐵 )
7	6	eqcoms	⊢ ( ( 𝐹 ‘ 𝐴 ) = V → ( 𝐹 ‘ 𝐴 ) = 𝐵 )