Theorem fveqvfvv 47936

Description: If a function's value at an argument is the universal class (which can never be the case because of fvex 6895), 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 6895	. . . 4 ⊢ (𝐹‘𝐴) ∈ V
2		eleq1a 2857	. . . 4 ⊢ ((𝐹‘𝐴) ∈ V → (V = (𝐹‘𝐴) → V ∈ V))
3	1, 2	ax-mp 5	. . 3 ⊢ (V = (𝐹‘𝐴) → V ∈ V)
4		vprc 5281	. . . 4 ⊢ ¬ V ∈ V
5	4	pm2.21i 120	. . 3 ⊢ (V ∈ V → (𝐹‘𝐴) = 𝐵)
6	3, 5	syl 18	. 2 ⊢ (V = (𝐹‘𝐴) → (𝐹‘𝐴) = 𝐵)
7	6	eqcoms 2770	1 ⊢ ((𝐹‘𝐴) = V → (𝐹‘𝐴) = 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3453  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-sn 4588  df-pr 4590  df-uni 4871  df-iota 6493  df-fv 6545

This theorem is used by:  afvpcfv0  48042