MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elunnel1 Structured version   Visualization version   GIF version

Theorem elunnel1 3903
Description: A member of a union that is not member of the first class, is member of the second class. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Assertion
Ref Expression
elunnel1 ((𝐴 ∈ (𝐵𝐶) ∧ ¬ 𝐴𝐵) → 𝐴𝐶)

Proof of Theorem elunnel1
StepHypRef Expression
1 elun 3902 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
21biimpi 206 . 2 (𝐴 ∈ (𝐵𝐶) → (𝐴𝐵𝐴𝐶))
32orcanai 993 1 ((𝐴 ∈ (𝐵𝐶) ∧ ¬ 𝐴𝐵) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  wo 826  wcel 2144  cun 3719
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-un 3726
This theorem is referenced by:  fsumsplitsn  14681  fprodsplitsn  14925  founiiun0  39891  infxrpnf  40184  cnrefiisplem  40567  dvnprodlem1  40673  fourierdlem70  40904  fourierdlem71  40905  fourierdlem80  40914  sge0splitmpt  41139  sge0iunmptlemfi  41141  nnfoctbdjlem  41183  hoidmvlelem2  41324  hoidmvlelem3  41325  pimrecltpos  41433
  Copyright terms: Public domain W3C validator