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

Theorem elin1d 4178
 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 4175 . 2 (𝑋 ∈ (𝐴𝐵) → 𝑋𝐴)
31, 2syl 17 1 (𝜑𝑋𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2107   ∩ cin 3938 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-v 3501  df-in 3946 This theorem is referenced by:  ordtypelem3  8976  ordtypelem4  8977  ordtypelem7  8980  infpwfien  9480  ttukeylem6  9928  fpwwe2lem12  10055  explecnv  15212  smuval2  15823  submrc  16891  coffth  17198  catcoppccl  17360  catcfuccl  17361  catcxpccl  17449  acsfiindd  17779  frgpnabllem2  18916  ablfac2  19133  mplind  20202  zringlpirlem2  20548  neiptoptop  21655  restbas  21682  subbascn  21778  cnconn  21946  clsconn  21954  conncompclo  21959  cldllycmp  22019  llycmpkgen2  22074  1stckgenlem  22077  txcls  22128  txcnp  22144  ptcnplem  22145  xkopt  22179  txconn  22213  basqtop  22235  tgqtop  22236  kqnrmlem1  22267  kqnrmlem2  22268  nrmhmph  22318  ptcmplem5  22580  restutop  22761  blin2  22954  met2ndci  23047  zdis  23339  reconnlem2  23350  cnheibor  23474  lebnum  23483  nmoleub2lem  23633  nmoleub2lem3  23634  nmoleub2lem2  23635  nmoleub3  23638  nmhmcn  23639  minveclem4  23950  ovolicc2lem5  24037  ioorcl  24093  ig1peu  24680  taylfvallem1  24860  tayl0  24865  ppisval  25595  ppinprm  25643  chtnprm  25645  chtleppi  25700  pclogsum  25705  chpchtsum  25709  chpub  25710  chebbnd1lem1  25959  chtppilimlem1  25963  rplogsum  26017  perpcom  26413  perpneq  26414  ragperp  26417  tocyc01  30674  cyc3evpm  30706  cycpmgcl  30709  cycpmconjslem2  30711  cyc3conja  30713  lbsdiflsp0  30908  esum2d  31238  ispisys2  31298  sigapisys  31300  sigapildsyslem  31306  sigapildsys  31307  eulerpartlemgvv  31520  tgoldbachgt  31820  fvineqsneq  34562  pibt2  34567  limclner  41793
 Copyright terms: Public domain W3C validator