Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fveqvfvv Structured version   Visualization version   GIF version

Theorem fveqvfvv 43800
 Description: If a function's value at an argument is the universal class (which can never be the case because of fvex 6668), 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
StepHypRef Expression
1 fvex 6668 . . . 4 (𝐹𝐴) ∈ V
2 eleq1a 2885 . . . 4 ((𝐹𝐴) ∈ V → (V = (𝐹𝐴) → V ∈ V))
31, 2ax-mp 5 . . 3 (V = (𝐹𝐴) → V ∈ V)
4 vprc 5187 . . . 4 ¬ V ∈ V
54pm2.21i 119 . . 3 (V ∈ V → (𝐹𝐴) = 𝐵)
63, 5syl 17 . 2 (V = (𝐹𝐴) → (𝐹𝐴) = 𝐵)
76eqcoms 2806 1 ((𝐹𝐴) = V → (𝐹𝐴) = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  Vcvv 3442  ‘cfv 6332 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3444  df-sbc 3723  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-sn 4529  df-pr 4531  df-uni 4805  df-iota 6291  df-fv 6340 This theorem is referenced by:  afvpcfv0  43870
 Copyright terms: Public domain W3C validator