Theorem fveqvfvv 47429

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3442  ‘cfv 6502

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-nul 5255

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-sn 4583  df-pr 4585  df-uni 4866  df-iota 6458  df-fv 6510

This theorem is referenced by:  afvpcfv0  47535