Theorem elin1d 4156

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 4153	. 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → 𝑋 ∈ 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝑋 ∈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2142   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911

This theorem is referenced by:  ordtypelem3  9468  ordtypelem4  9469  ordtypelem7  9472  infpwfien  10018  ttukeylem6  10471  fpwwe2lem11  10599  explecnv  15895  smuval2  16516  submrc  17660  coffth  17971  catcbascl  18145  acsfiindd  18585  frgpnabllem2  19914  ablfac2  20131  idomcringd  20777  2idllidld  21324  zringlpirlem2  21515  mplind  22123  neiptoptop  23191  restbas  23218  subbascn  23314  cnconn  23482  clsconn  23490  conncompclo  23495  cldllycmp  23555  llycmpkgen2  23610  1stckgenlem  23613  txcls  23664  txcnp  23680  ptcnplem  23681  xkopt  23715  txconn  23749  basqtop  23771  tgqtop  23772  kqnrmlem1  23803  kqnrmlem2  23804  nrmhmph  23854  ptcmplem5  24116  restutop  24297  blin2  24489  met2ndci  24582  zdis  24877  reconnlem2  24888  cnheibor  25017  lebnum  25026  nmoleub2lem  25176  nmoleub2lem3  25177  nmoleub2lem2  25178  nmoleub3  25181  nmhmcn  25182  minveclem4  25494  ovolicc2lem5  25583  ioorcl  25639  ig1peu  26235  taylfvallem1  26420  tayl0  26425  ppisval  27168  ppinprm  27216  chtnprm  27218  chtleppi  27274  pclogsum  27279  chpchtsum  27283  chpub  27284  chebbnd1lem1  27533  chtppilimlem1  27537  rplogsum  27591  tglnpt4  28824  perpcom  28886  perpneq  28887  ragperp  28890  lnincplng  28991  tocyc01  33298  cyc3evpm  33330  cycpmgcl  33333  cycpmconjslem2  33335  cyc3conja  33337  idomrcanOLD  33466  ssdifidlprm  33645  mxidlirred  33660  dflringlem3  33692  dflring4  33694  rprmirredb  33728  pidufd  33739  1arithufdlem4  33743  exsslsb  33894  lbsdiflsp0  33923  esum2d  34390  ispisys2  34450  sigapisys  34452  sigapildsyslem  34458  sigapildsys  34459  eulerpartlemgvv  34673  tgoldbachgt  34957  weiunfrlem  36824  weiunfr  36827  dfttc4  36890  fvineqsneq  37906  pibt2  37911  limclner  46225  fourierdlem49  46729  iinfconstbas  49687  ffthoppf  49786  thincciso  50074  termcterm2  50135  termcciso  50137  termccisoeu  50138  termfucterm  50165  uobeqterm  50167