Theorem fveqvfvv 45245

Description: If a function's value at an argument is the universal class (which can never be the case because of fvex 6855), 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 119). (Contributed by Alexander van der Vekens, 26-May-2017.)

Assertion

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

Proof of Theorem fveqvfvv

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3445  ‘cfv 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256  ax-nul 5263

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-sn 4587  df-pr 4589  df-uni 4866  df-iota 6448  df-fv 6504

This theorem is referenced by:  afvpcfv0  45349