Theorem elin1d 4133

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

Syntax hints:   → wi 4   ∈ wcel 2119   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890

This theorem is referenced by:  ordtypelem3  9425  ordtypelem4  9426  ordtypelem7  9429  infpwfien  9975  ttukeylem6  10427  fpwwe2lem11  10555  explecnv  15821  smuval2  16442  submrc  17585  coffth  17896  catcbascl  18070  acsfiindd  18510  frgpnabllem2  19840  ablfac2  20057  idomcringd  20699  2idllidld  21247  zringlpirlem2  21438  mplind  22046  neiptoptop  23114  restbas  23141  subbascn  23237  cnconn  23405  clsconn  23413  conncompclo  23418  cldllycmp  23478  llycmpkgen2  23533  1stckgenlem  23536  txcls  23587  txcnp  23603  ptcnplem  23604  xkopt  23638  txconn  23672  basqtop  23694  tgqtop  23695  kqnrmlem1  23726  kqnrmlem2  23727  nrmhmph  23777  ptcmplem5  24039  restutop  24220  blin2  24412  met2ndci  24505  zdis  24800  reconnlem2  24811  cnheibor  24940  lebnum  24949  nmoleub2lem  25099  nmoleub2lem3  25100  nmoleub2lem2  25101  nmoleub3  25104  nmhmcn  25105  minveclem4  25417  ovolicc2lem5  25506  ioorcl  25562  ig1peu  26158  taylfvallem1  26340  tayl0  26345  ppisval  27085  ppinprm  27133  chtnprm  27135  chtleppi  27191  pclogsum  27196  chpchtsum  27200  chpub  27201  chebbnd1lem1  27450  chtppilimlem1  27454  rplogsum  27508  perpcom  28799  perpneq  28800  ragperp  28803  tocyc01  33199  cyc3evpm  33231  cycpmgcl  33234  cycpmconjslem2  33236  cyc3conja  33238  idomrcanOLD  33363  unitpidl1  33507  ssdifidlprm  33541  mxidlirredi  33554  mxidlirred  33555  rprmirredb  33615  pidufd  33626  1arithufdlem4  33630  exsslsb  33781  lbsdiflsp0  33810  esum2d  34277  ispisys2  34337  sigapisys  34339  sigapildsyslem  34345  sigapildsys  34346  eulerpartlemgvv  34560  tgoldbachgt  34847  weiunfrlem  36692  weiunfr  36695  dfttc4  36758  fvineqsneq  37774  pibt2  37779  limclner  46094  iinfconstbas  49556  ffthoppf  49655  thincciso  49943  termcterm2  50004  termcciso  50006  termccisoeu  50007  termfucterm  50034  uobeqterm  50036