Theorem elin1d 4163

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

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

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920

This theorem is referenced by:  ordtypelem3  9465  ordtypelem4  9466  ordtypelem7  9469  infpwfien  10007  ttukeylem6  10459  fpwwe2lem11  10586  explecnv  15761  smuval2  16373  submrc  17522  coffth  17837  catcbascl  18012  catcoppcclOLD  18018  catcfucclOLD  18020  catcxpcclOLD  18110  acsfiindd  18456  frgpnabllem2  19666  ablfac2  19882  zringlpirlem2  20921  mplind  21515  neiptoptop  22519  restbas  22546  subbascn  22642  cnconn  22810  clsconn  22818  conncompclo  22823  cldllycmp  22883  llycmpkgen2  22938  1stckgenlem  22941  txcls  22992  txcnp  23008  ptcnplem  23009  xkopt  23043  txconn  23077  basqtop  23099  tgqtop  23100  kqnrmlem1  23131  kqnrmlem2  23132  nrmhmph  23182  ptcmplem5  23444  restutop  23626  blin2  23819  met2ndci  23915  zdis  24216  reconnlem2  24227  cnheibor  24355  lebnum  24364  nmoleub2lem  24514  nmoleub2lem3  24515  nmoleub2lem2  24516  nmoleub3  24519  nmhmcn  24520  minveclem4  24833  ovolicc2lem5  24922  ioorcl  24978  ig1peu  25573  taylfvallem1  25753  tayl0  25758  ppisval  26490  ppinprm  26538  chtnprm  26540  chtleppi  26595  pclogsum  26600  chpchtsum  26604  chpub  26605  chebbnd1lem1  26854  chtppilimlem1  26858  rplogsum  26912  perpcom  27718  perpneq  27719  ragperp  27722  tocyc01  32037  cyc3evpm  32069  cycpmgcl  32072  cycpmconjslem2  32074  cyc3conja  32076  lbsdiflsp0  32408  esum2d  32781  ispisys2  32841  sigapisys  32843  sigapildsyslem  32849  sigapildsys  32850  eulerpartlemgvv  33065  tgoldbachgt  33365  fvineqsneq  35956  pibt2  35961  limclner  44012  thincciso  47189