Theorem fveqvfvv 48203

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

Assertion

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

Proof of Theorem fveqvfvv

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  Vcvv 3450  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-sn 4585  df-pr 4587  df-uni 4867  df-iota 6494  df-fv 6546

This theorem is used by:  afvpcfv0  48309