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

Theorem elunnel1 3976
 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 3975 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
21biimpi 208 . 2 (𝐴 ∈ (𝐵𝐶) → (𝐴𝐵𝐴𝐶))
32orcanai 988 1 ((𝐴 ∈ (𝐵𝐶) ∧ ¬ 𝐴𝐵) → 𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 386   ∨ wo 836   ∈ wcel 2106   ∪ cun 3789 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-v 3399  df-un 3796 This theorem is referenced by:  fsumsplitsn  14881  fprodsplitsn  15122  founiiun0  40293  infxrpnf  40573  cnrefiisplem  40962  dvnprodlem1  41082  fourierdlem70  41313  fourierdlem71  41314  fourierdlem80  41323  sge0splitmpt  41545  sge0iunmptlemfi  41547  nnfoctbdjlem  41589  hoidmvlelem2  41730  hoidmvlelem3  41731  pimrecltpos  41839
 Copyright terms: Public domain W3C validator