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

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

Proof of Theorem elunnel1
StepHypRef Expression
1 elun 4147 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
21biimpi 215 . 2 (𝐴 ∈ (𝐵𝐶) → (𝐴𝐵𝐴𝐶))
32orcanai 999 1 ((𝐴 ∈ (𝐵𝐶) ∧ ¬ 𝐴𝐵) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  wo 843  wcel 2104  cun 3945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3952
This theorem is referenced by:  fsumsplitsn  15694  fprodsplitsn  15937  founiiun0  44187  infxrpnf  44454  cnrefiisplem  44843  dvnprodlem1  44960  fourierdlem70  45190  fourierdlem71  45191  fourierdlem80  45200  sge0splitmpt  45425  sge0iunmptlemfi  45427  nnfoctbdjlem  45469  hoidmvlelem2  45610  hoidmvlelem3  45611  pimrecltpos  45722
  Copyright terms: Public domain W3C validator