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 2113   ∩ cin 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908

This theorem is referenced by:  ordtypelem3  9425  ordtypelem4  9426  ordtypelem7  9429  infpwfien  9972  ttukeylem6  10424  fpwwe2lem11  10552  explecnv  15788  smuval2  16409  submrc  17551  coffth  17862  catcbascl  18036  acsfiindd  18476  frgpnabllem2  19803  ablfac2  20020  idomcringd  20660  2idllidld  21209  zringlpirlem2  21418  mplind  22025  neiptoptop  23075  restbas  23102  subbascn  23198  cnconn  23366  clsconn  23374  conncompclo  23379  cldllycmp  23439  llycmpkgen2  23494  1stckgenlem  23497  txcls  23548  txcnp  23564  ptcnplem  23565  xkopt  23599  txconn  23633  basqtop  23655  tgqtop  23656  kqnrmlem1  23687  kqnrmlem2  23688  nrmhmph  23738  ptcmplem5  24000  restutop  24181  blin2  24373  met2ndci  24466  zdis  24761  reconnlem2  24772  cnheibor  24910  lebnum  24919  nmoleub2lem  25070  nmoleub2lem3  25071  nmoleub2lem2  25072  nmoleub3  25075  nmhmcn  25076  minveclem4  25388  ovolicc2lem5  25478  ioorcl  25534  ig1peu  26136  taylfvallem1  26320  tayl0  26325  ppisval  27070  ppinprm  27118  chtnprm  27120  chtleppi  27177  pclogsum  27182  chpchtsum  27186  chpub  27187  chebbnd1lem1  27436  chtppilimlem1  27440  rplogsum  27494  perpcom  28785  perpneq  28786  ragperp  28789  tocyc01  33200  cyc3evpm  33232  cycpmgcl  33235  cycpmconjslem2  33237  cyc3conja  33239  idomrcanOLD  33364  unitpidl1  33505  ssdifidlprm  33539  mxidlirredi  33552  mxidlirred  33553  rprmirredb  33613  pidufd  33624  1arithufdlem4  33628  exsslsb  33753  lbsdiflsp0  33783  esum2d  34250  ispisys2  34310  sigapisys  34312  sigapildsyslem  34318  sigapildsys  34319  eulerpartlemgvv  34533  tgoldbachgt  34820  weiunfrlem  36658  weiunfr  36661  fvineqsneq  37617  pibt2  37622  limclner  45895  iinfconstbas  49311  ffthoppf  49410  thincciso  49698  termcterm2  49759  termcciso  49761  termccisoeu  49762  termfucterm  49789  uobeqterm  49791