Theorem elin1d 4155

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

Step	Hyp	Ref	Expression
1		elin1d.1	. 2 ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))
2		elinel1 4152	. 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → 𝑋 ∈ 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝑋 ∈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3902

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-in 3910

This theorem is referenced by:  ordtypelem3  9412  ordtypelem4  9413  ordtypelem7  9416  infpwfien  9956  ttukeylem6  10408  fpwwe2lem11  10535  explecnv  15772  smuval2  16393  submrc  17534  coffth  17845  catcbascl  18019  acsfiindd  18459  frgpnabllem2  19753  ablfac2  19970  idomcringd  20612  2idllidld  21161  zringlpirlem2  21370  mplind  21975  neiptoptop  23016  restbas  23043  subbascn  23139  cnconn  23307  clsconn  23315  conncompclo  23320  cldllycmp  23380  llycmpkgen2  23435  1stckgenlem  23438  txcls  23489  txcnp  23505  ptcnplem  23506  xkopt  23540  txconn  23574  basqtop  23596  tgqtop  23597  kqnrmlem1  23628  kqnrmlem2  23629  nrmhmph  23679  ptcmplem5  23941  restutop  24123  blin2  24315  met2ndci  24408  zdis  24703  reconnlem2  24714  cnheibor  24852  lebnum  24861  nmoleub2lem  25012  nmoleub2lem3  25013  nmoleub2lem2  25014  nmoleub3  25017  nmhmcn  25018  minveclem4  25330  ovolicc2lem5  25420  ioorcl  25476  ig1peu  26078  taylfvallem1  26262  tayl0  26267  ppisval  27012  ppinprm  27060  chtnprm  27062  chtleppi  27119  pclogsum  27124  chpchtsum  27128  chpub  27129  chebbnd1lem1  27378  chtppilimlem1  27382  rplogsum  27436  perpcom  28658  perpneq  28659  ragperp  28662  tocyc01  33060  cyc3evpm  33092  cycpmgcl  33095  cycpmconjslem2  33097  cyc3conja  33099  idomrcanOLD  33221  unitpidl1  33361  ssdifidlprm  33395  mxidlirredi  33408  mxidlirred  33409  rprmirredb  33469  pidufd  33480  1arithufdlem4  33484  exsslsb  33563  lbsdiflsp0  33593  esum2d  34060  ispisys2  34120  sigapisys  34122  sigapildsyslem  34128  sigapildsys  34129  eulerpartlemgvv  34344  tgoldbachgt  34631  weiunfrlem  36442  weiunfr  36445  fvineqsneq  37390  pibt2  37395  limclner  45636  iinfconstbas  49055  ffthoppf  49154  thincciso  49442  termcterm2  49503  termcciso  49505  termccisoeu  49506  termfucterm  49533  uobeqterm  49535