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

Theorem elin1d 4172
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
elin1d (𝜑𝑋𝐴)

Proof of Theorem elin1d
StepHypRef Expression
1 elin1d.1 . 2 (𝜑𝑋 ∈ (𝐴𝐵))
2 elinel1 4169 . 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:  ordtypelem3  8972  ordtypelem4  8973  ordtypelem7  8976  infpwfien  9476  ttukeylem6  9924  fpwwe2lem12  10051  explecnv  15208  smuval2  15819  submrc  16887  coffth  17194  catcoppccl  17356  catcfuccl  17357  catcxpccl  17445  acsfiindd  17775  frgpnabllem2  18923  ablfac2  19140  mplind  20210  zringlpirlem2  20560  neiptoptop  21667  restbas  21694  subbascn  21790  cnconn  21958  clsconn  21966  conncompclo  21971  cldllycmp  22031  llycmpkgen2  22086  1stckgenlem  22089  txcls  22140  txcnp  22156  ptcnplem  22157  xkopt  22191  txconn  22225  basqtop  22247  tgqtop  22248  kqnrmlem1  22279  kqnrmlem2  22280  nrmhmph  22330  ptcmplem5  22592  restutop  22773  blin2  22966  met2ndci  23059  zdis  23351  reconnlem2  23362  cnheibor  23486  lebnum  23495  nmoleub2lem  23645  nmoleub2lem3  23646  nmoleub2lem2  23647  nmoleub3  23650  nmhmcn  23651  minveclem4  23962  ovolicc2lem5  24049  ioorcl  24105  ig1peu  24692  taylfvallem1  24872  tayl0  24877  ppisval  25608  ppinprm  25656  chtnprm  25658  chtleppi  25713  pclogsum  25718  chpchtsum  25722  chpub  25723  chebbnd1lem1  25972  chtppilimlem1  25976  rplogsum  26030  perpcom  26426  perpneq  26427  ragperp  26430  tocyc01  30687  cyc3evpm  30719  cycpmgcl  30722  cycpmconjslem2  30724  cyc3conja  30726  lbsdiflsp0  30921  esum2d  31251  ispisys2  31311  sigapisys  31313  sigapildsyslem  31319  sigapildsys  31320  eulerpartlemgvv  31533  tgoldbachgt  31833  fvineqsneq  34575  pibt2  34580  limclner  41808
  Copyright terms: Public domain W3C validator