Theorem elin1d 4154

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

Syntax hints:   → wi 4   ∈ wcel 2113   ∩ cin 3898

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906

This theorem is referenced by:  ordtypelem3  9423  ordtypelem4  9424  ordtypelem7  9427  infpwfien  9970  ttukeylem6  10422  fpwwe2lem11  10550  explecnv  15786  smuval2  16407  submrc  17549  coffth  17860  catcbascl  18034  acsfiindd  18474  frgpnabllem2  19801  ablfac2  20018  idomcringd  20658  2idllidld  21207  zringlpirlem2  21416  mplind  22023  neiptoptop  23073  restbas  23100  subbascn  23196  cnconn  23364  clsconn  23372  conncompclo  23377  cldllycmp  23437  llycmpkgen2  23492  1stckgenlem  23495  txcls  23546  txcnp  23562  ptcnplem  23563  xkopt  23597  txconn  23631  basqtop  23653  tgqtop  23654  kqnrmlem1  23685  kqnrmlem2  23686  nrmhmph  23736  ptcmplem5  23998  restutop  24179  blin2  24371  met2ndci  24464  zdis  24759  reconnlem2  24770  cnheibor  24908  lebnum  24917  nmoleub2lem  25068  nmoleub2lem3  25069  nmoleub2lem2  25070  nmoleub3  25073  nmhmcn  25074  minveclem4  25386  ovolicc2lem5  25476  ioorcl  25532  ig1peu  26134  taylfvallem1  26318  tayl0  26323  ppisval  27068  ppinprm  27116  chtnprm  27118  chtleppi  27175  pclogsum  27180  chpchtsum  27184  chpub  27185  chebbnd1lem1  27434  chtppilimlem1  27438  rplogsum  27492  perpcom  28734  perpneq  28735  ragperp  28738  tocyc01  33149  cyc3evpm  33181  cycpmgcl  33184  cycpmconjslem2  33186  cyc3conja  33188  idomrcanOLD  33313  unitpidl1  33454  ssdifidlprm  33488  mxidlirredi  33501  mxidlirred  33502  rprmirredb  33562  pidufd  33573  1arithufdlem4  33577  exsslsb  33702  lbsdiflsp0  33732  esum2d  34199  ispisys2  34259  sigapisys  34261  sigapildsyslem  34267  sigapildsys  34268  eulerpartlemgvv  34482  tgoldbachgt  34769  weiunfrlem  36607  weiunfr  36610  fvineqsneq  37556  pibt2  37561  limclner  45837  iinfconstbas  49253  ffthoppf  49352  thincciso  49640  termcterm2  49701  termcciso  49703  termccisoeu  49704  termfucterm  49731  uobeqterm  49733