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

Theorem elunnel1 4154
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 4153 . . 3 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
21biimpi 216 . 2 (𝐴 ∈ (𝐵𝐶) → (𝐴𝐵𝐴𝐶))
32orcanai 1005 1 ((𝐴 ∈ (𝐵𝐶) ∧ ¬ 𝐴𝐵) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 848  wcel 2108  cun 3949
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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956
This theorem is referenced by:  fsumsplitsn  15780  fprodsplitsn  16025  founiiun0  45195  infxrpnf  45457  cnrefiisplem  45844  dvnprodlem1  45961  fourierdlem70  46191  fourierdlem71  46192  fourierdlem80  46201  sge0splitmpt  46426  sge0iunmptlemfi  46428  nnfoctbdjlem  46470  hoidmvlelem2  46611  hoidmvlelem3  46612  pimrecltpos  46723
  Copyright terms: Public domain W3C validator