Theorem elin1d 4167

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921

This theorem is referenced by:  ordtypelem3  9473  ordtypelem4  9474  ordtypelem7  9477  infpwfien  10015  ttukeylem6  10467  fpwwe2lem11  10594  explecnv  15831  smuval2  16452  submrc  17589  coffth  17900  catcbascl  18074  acsfiindd  18512  frgpnabllem2  19804  ablfac2  20021  idomcringd  20636  2idllidld  21164  zringlpirlem2  21373  mplind  21977  neiptoptop  23018  restbas  23045  subbascn  23141  cnconn  23309  clsconn  23317  conncompclo  23322  cldllycmp  23382  llycmpkgen2  23437  1stckgenlem  23440  txcls  23491  txcnp  23507  ptcnplem  23508  xkopt  23542  txconn  23576  basqtop  23598  tgqtop  23599  kqnrmlem1  23630  kqnrmlem2  23631  nrmhmph  23681  ptcmplem5  23943  restutop  24125  blin2  24317  met2ndci  24410  zdis  24705  reconnlem2  24716  cnheibor  24854  lebnum  24863  nmoleub2lem  25014  nmoleub2lem3  25015  nmoleub2lem2  25016  nmoleub3  25019  nmhmcn  25020  minveclem4  25332  ovolicc2lem5  25422  ioorcl  25478  ig1peu  26080  taylfvallem1  26264  tayl0  26269  ppisval  27014  ppinprm  27062  chtnprm  27064  chtleppi  27121  pclogsum  27126  chpchtsum  27130  chpub  27131  chebbnd1lem1  27380  chtppilimlem1  27384  rplogsum  27438  perpcom  28640  perpneq  28641  ragperp  28644  tocyc01  33075  cyc3evpm  33107  cycpmgcl  33110  cycpmconjslem2  33112  cyc3conja  33114  idomrcanOLD  33232  unitpidl1  33395  ssdifidlprm  33429  mxidlirredi  33442  mxidlirred  33443  rprmirredb  33503  pidufd  33514  1arithufdlem4  33518  exsslsb  33592  lbsdiflsp0  33622  esum2d  34083  ispisys2  34143  sigapisys  34145  sigapildsyslem  34151  sigapildsys  34152  eulerpartlemgvv  34367  tgoldbachgt  34654  weiunfrlem  36452  weiunfr  36455  fvineqsneq  37400  pibt2  37405  limclner  45649  iinfconstbas  49055  ffthoppf  49154  thincciso  49442  termcterm2  49503  termcciso  49505  termccisoeu  49506  termfucterm  49533  uobeqterm  49535