Users' Mathboxes 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 39746
Description: If a function's value at an argument is the universal class (which can never be the case because of fvex 5996), 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 114). (Contributed by Alexander van der Vekens, 26-May-2017.)
Assertion
Ref Expression
fveqvfvv ((𝐹𝐴) = V → (𝐹𝐴) = 𝐵)

Proof of Theorem fveqvfvv
StepHypRef Expression
1 fvex 5996 . . . 4 (𝐹𝐴) ∈ V
2 eleq1a 2587 . . . 4 ((𝐹𝐴) ∈ V → (V = (𝐹𝐴) → V ∈ V))
31, 2ax-mp 5 . . 3 (V = (𝐹𝐴) → V ∈ V)
4 vprc 4623 . . . 4 ¬ V ∈ V
54pm2.21i 114 . . 3 (V ∈ V → (𝐹𝐴) = 𝐵)
63, 5syl 17 . 2 (V = (𝐹𝐴) → (𝐹𝐴) = 𝐵)
76eqcoms 2522 1 ((𝐹𝐴) = V → (𝐹𝐴) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1938  Vcvv 3077  cfv 5689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rex 2806  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-sn 4029  df-pr 4031  df-uni 4271  df-iota 5653  df-fv 5697
This theorem is referenced by:  afvpcfv0  39769
  Copyright terms: Public domain W3C validator