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

Theorem afvfv0bi 42787
Description: The function's value at an argument is the empty set if and only if the value of the alternative function at this argument is either the empty set or the universe. (Contributed by Alexander van der Vekens, 25-May-2017.)
Assertion
Ref Expression
afvfv0bi ((𝐹𝐴) = ∅ ↔ ((𝐹'''𝐴) = ∅ ∨ (𝐹'''𝐴) = V))

Proof of Theorem afvfv0bi
StepHypRef Expression
1 ioran 967 . . . 4 (¬ ((𝐹'''𝐴) = ∅ ∨ (𝐹'''𝐴) = V) ↔ (¬ (𝐹'''𝐴) = ∅ ∧ ¬ (𝐹'''𝐴) = V))
2 df-ne 2963 . . . . . . 7 ((𝐹'''𝐴) ≠ V ↔ ¬ (𝐹'''𝐴) = V)
3 afvnufveq 42782 . . . . . . 7 ((𝐹'''𝐴) ≠ V → (𝐹'''𝐴) = (𝐹𝐴))
42, 3sylbir 227 . . . . . 6 (¬ (𝐹'''𝐴) = V → (𝐹'''𝐴) = (𝐹𝐴))
5 eqeq1 2777 . . . . . . . 8 ((𝐹'''𝐴) = (𝐹𝐴) → ((𝐹'''𝐴) = ∅ ↔ (𝐹𝐴) = ∅))
65notbid 310 . . . . . . 7 ((𝐹'''𝐴) = (𝐹𝐴) → (¬ (𝐹'''𝐴) = ∅ ↔ ¬ (𝐹𝐴) = ∅))
76biimpd 221 . . . . . 6 ((𝐹'''𝐴) = (𝐹𝐴) → (¬ (𝐹'''𝐴) = ∅ → ¬ (𝐹𝐴) = ∅))
84, 7syl 17 . . . . 5 (¬ (𝐹'''𝐴) = V → (¬ (𝐹'''𝐴) = ∅ → ¬ (𝐹𝐴) = ∅))
98impcom 399 . . . 4 ((¬ (𝐹'''𝐴) = ∅ ∧ ¬ (𝐹'''𝐴) = V) → ¬ (𝐹𝐴) = ∅)
101, 9sylbi 209 . . 3 (¬ ((𝐹'''𝐴) = ∅ ∨ (𝐹'''𝐴) = V) → ¬ (𝐹𝐴) = ∅)
1110con4i 114 . 2 ((𝐹𝐴) = ∅ → ((𝐹'''𝐴) = ∅ ∨ (𝐹'''𝐴) = V))
12 afv0fv0 42784 . . 3 ((𝐹'''𝐴) = ∅ → (𝐹𝐴) = ∅)
13 afvpcfv0 42781 . . 3 ((𝐹'''𝐴) = V → (𝐹𝐴) = ∅)
1412, 13jaoi 844 . 2 (((𝐹'''𝐴) = ∅ ∨ (𝐹'''𝐴) = V) → (𝐹𝐴) = ∅)
1511, 14impbii 201 1 ((𝐹𝐴) = ∅ ↔ ((𝐹'''𝐴) = ∅ ∨ (𝐹'''𝐴) = V))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  wo 834   = wceq 1508  wne 2962  Vcvv 3410  c0 4173  cfv 6186  '''cafv 42752
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-fal 1521  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-int 4747  df-br 4927  df-opab 4989  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-res 5416  df-iota 6150  df-fun 6188  df-fv 6194  df-aiota 42721  df-dfat 42754  df-afv 42755
This theorem is referenced by:  aovov0bi  42831
  Copyright terms: Public domain W3C validator