Theorem elin1d 4136

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

Syntax hints:   → wi 4   ∈ wcel 2121   ∩ cin 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-in 3892

This theorem is referenced by:  ordtypelem3  9429  ordtypelem4  9430  ordtypelem7  9433  infpwfien  9979  ttukeylem6  10431  fpwwe2lem11  10559  explecnv  15825  smuval2  16446  submrc  17589  coffth  17900  catcbascl  18074  acsfiindd  18514  frgpnabllem2  19844  ablfac2  20061  idomcringd  20703  2idllidld  21251  zringlpirlem2  21442  mplind  22050  neiptoptop  23118  restbas  23145  subbascn  23241  cnconn  23409  clsconn  23417  conncompclo  23422  cldllycmp  23482  llycmpkgen2  23537  1stckgenlem  23540  txcls  23591  txcnp  23607  ptcnplem  23608  xkopt  23642  txconn  23676  basqtop  23698  tgqtop  23699  kqnrmlem1  23730  kqnrmlem2  23731  nrmhmph  23781  ptcmplem5  24043  restutop  24224  blin2  24416  met2ndci  24509  zdis  24804  reconnlem2  24815  cnheibor  24944  lebnum  24953  nmoleub2lem  25103  nmoleub2lem3  25104  nmoleub2lem2  25105  nmoleub3  25108  nmhmcn  25109  minveclem4  25421  ovolicc2lem5  25510  ioorcl  25566  ig1peu  26162  taylfvallem1  26344  tayl0  26349  ppisval  27089  ppinprm  27137  chtnprm  27139  chtleppi  27195  pclogsum  27200  chpchtsum  27204  chpub  27205  chebbnd1lem1  27454  chtppilimlem1  27458  rplogsum  27512  perpcom  28803  perpneq  28804  ragperp  28807  tocyc01  33203  cyc3evpm  33235  cycpmgcl  33238  cycpmconjslem2  33240  cyc3conja  33242  idomrcanOLD  33367  ssdifidlprm  33545  mxidlirred  33559  dflringlem3  33591  dflring4  33593  rprmirredb  33627  pidufd  33638  1arithufdlem4  33642  exsslsb  33793  lbsdiflsp0  33822  esum2d  34289  ispisys2  34349  sigapisys  34351  sigapildsyslem  34357  sigapildsys  34358  eulerpartlemgvv  34572  tgoldbachgt  34859  weiunfrlem  36707  weiunfr  36710  dfttc4  36773  fvineqsneq  37789  pibt2  37794  limclner  46108  iinfconstbas  49570  ffthoppf  49669  thincciso  49957  termcterm2  50018  termcciso  50020  termccisoeu  50021  termfucterm  50048  uobeqterm  50050