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

Theorem elin2d 4173
Description: Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)
Hypothesis
Ref Expression
elin1d.1 (𝜑𝑋 ∈ (𝐴𝐵))
Assertion
Ref Expression
elin2d (𝜑𝑋𝐵)

Proof of Theorem elin2d
StepHypRef Expression
1 elin1d.1 . 2 (𝜑𝑋 ∈ (𝐴𝐵))
2 elinel2 4170 . 2 (𝑋 ∈ (𝐴𝐵) → 𝑋𝐵)
31, 2syl 17 1 (𝜑𝑋𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cin 3932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-in 3940
This theorem is referenced by:  f1opwfi  8816  elfiun  8882  ordtypelem3  8972  infpwfien  9476  ttukeylem6  9924  fpwwe2lem12  10051  explecnv  15208  bitsinv1  15779  smuval2  15819  firest  16694  sscres  17081  funcres2c  17159  coffth  17194  rescfth  17195  catcoppccl  17356  catcfuccl  17357  catcxpccl  17445  psssdm2  17813  frgpnabllem2  18923  sralmod  19888  mplind  20210  zringlpirlem3  20561  neiptoptop  21667  restbas  21694  ordtrest  21738  subbascn  21790  lmss  21834  cnconn  21958  clsconn  21966  conncompclo  21971  subislly  22017  cldllycmp  22031  1stckgenlem  22089  txcls  22140  txcnp  22156  txtube  22176  txcmplem1  22177  txkgen  22188  xkopt  22191  xkococnlem  22195  txconn  22225  basqtop  22247  tgqtop  22248  kqnrmlem1  22279  kqnrmlem2  22280  nrmhmph  22330  uzrest  22433  alexsubALTlem3  22585  ptcmplem2  22589  tsmslem1  22664  tsmsxplem1  22688  tsmsxplem2  22689  tsmsxp  22690  blin2  22966  met2ndci  23059  zdis  23351  reconnlem2  23362  reconn  23363  xrge0gsumle  23368  cnheibor  23486  lebnum  23495  nmoleub2lem3  23646  nmoleub3  23650  caussi  23827  minveclem4b  23961  minveclem4  23962  ovolfcl  23994  ovolfioo  23995  ovolficc  23996  ovolficcss  23997  ovolfsval  23998  ovoliunlem1  24030  ovolicc2lem4  24048  ovolicc2lem5  24049  uniiccdif  24106  uniioovol  24107  uniiccvol  24108  uniioombllem2a  24110  uniioombllem3a  24112  uniioombllem4  24114  uniioombllem5  24115  uniioombllem6  24116  vitalilem2  24137  vitalilem4  24139  ig1peu  24692  taylfvallem1  24872  tayl0  24877  ppisval  25608  chtf  25612  efchtcl  25615  chtge0  25616  ppinprm  25656  chtprm  25657  chtnprm  25658  chtwordi  25660  chtdif  25662  efchtdvds  25663  chtlepsi  25709  chtleppi  25713  pclogsum  25718  chpval2  25721  chpchtsum  25722  chpub  25723  chebbnd1lem1  25972  chtppilimlem1  25976  rplogsumlem2  25988  perpneq  26427  ragperp  26430  tocyc01  30687  cyc3evpm  30719  cycpmconjslem2  30724  cyc3conja  30726  lbsdiflsp0  30921  esum2d  31251  ispisys2  31311  sigapisys  31313  sigapildsyslem  31319  sigapildsys  31320  sseqf  31549  tgoldbachgt  31833  bnj1172  32170  cnrefiisplem  41986  hoiqssbllem3  42783  smflimlem3  42926
  Copyright terms: Public domain W3C validator