Theorem elin1d 4132

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

Syntax hints:   → wi 4   ∈ wcel 2106   ∩ cin 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894

This theorem is referenced by:  ordtypelem3  9279  ordtypelem4  9280  ordtypelem7  9283  infpwfien  9818  ttukeylem6  10270  fpwwe2lem11  10397  explecnv  15577  smuval2  16189  submrc  17337  coffth  17652  catcbascl  17827  catcoppcclOLD  17833  catcfucclOLD  17835  catcxpcclOLD  17925  acsfiindd  18271  frgpnabllem2  19475  ablfac2  19692  zringlpirlem2  20685  mplind  21278  neiptoptop  22282  restbas  22309  subbascn  22405  cnconn  22573  clsconn  22581  conncompclo  22586  cldllycmp  22646  llycmpkgen2  22701  1stckgenlem  22704  txcls  22755  txcnp  22771  ptcnplem  22772  xkopt  22806  txconn  22840  basqtop  22862  tgqtop  22863  kqnrmlem1  22894  kqnrmlem2  22895  nrmhmph  22945  ptcmplem5  23207  restutop  23389  blin2  23582  met2ndci  23678  zdis  23979  reconnlem2  23990  cnheibor  24118  lebnum  24127  nmoleub2lem  24277  nmoleub2lem3  24278  nmoleub2lem2  24279  nmoleub3  24282  nmhmcn  24283  minveclem4  24596  ovolicc2lem5  24685  ioorcl  24741  ig1peu  25336  taylfvallem1  25516  tayl0  25521  ppisval  26253  ppinprm  26301  chtnprm  26303  chtleppi  26358  pclogsum  26363  chpchtsum  26367  chpub  26368  chebbnd1lem1  26617  chtppilimlem1  26621  rplogsum  26675  perpcom  27074  perpneq  27075  ragperp  27078  tocyc01  31385  cyc3evpm  31417  cycpmgcl  31420  cycpmconjslem2  31422  cyc3conja  31424  lbsdiflsp0  31707  esum2d  32061  ispisys2  32121  sigapisys  32123  sigapildsyslem  32129  sigapildsys  32130  eulerpartlemgvv  32343  tgoldbachgt  32643  fvineqsneq  35583  pibt2  35588  limclner  43192  thincciso  46330