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

Theorem elunnel1 4080
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 4079 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
21biimpi 219 . 2 (𝐴 ∈ (𝐵𝐶) → (𝐴𝐵𝐴𝐶))
32orcanai 1000 1 ((𝐴 ∈ (𝐵𝐶) ∧ ¬ 𝐴𝐵) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wo 844  wcel 2112  cun 3882
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 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889
This theorem is referenced by:  fsumsplitsn  15096  fprodsplitsn  15339  founiiun0  41814  infxrpnf  42081  cnrefiisplem  42468  dvnprodlem1  42585  fourierdlem70  42815  fourierdlem71  42816  fourierdlem80  42825  sge0splitmpt  43047  sge0iunmptlemfi  43049  nnfoctbdjlem  43091  hoidmvlelem2  43232  hoidmvlelem3  43233  pimrecltpos  43341
  Copyright terms: Public domain W3C validator