Theorem elin1d 4165

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920

This theorem is referenced by:  ordtypelem3  9481  ordtypelem4  9482  ordtypelem7  9485  infpwfien  10045  ttukeylem6  10497  fpwwe2lem11  10625  explecnv  15918  smuval2  16539  submrc  17683  coffth  17994  catcbascl  18168  acsfiindd  18608  frgpnabllem2  19943  ablfac2  20160  idomcringd  20810  2idllidld  21363  ssdifidlprm  21454  zringlpirlem2  21581  mplind  22189  neiptoptop  23256  restbas  23283  subbascn  23379  cnconn  23547  clsconn  23555  conncompclo  23560  cldllycmp  23620  llycmpkgen2  23675  1stckgenlem  23678  txcls  23729  txcnp  23745  ptcnplem  23746  xkopt  23780  txconn  23814  basqtop  23836  tgqtop  23837  kqnrmlem1  23868  kqnrmlem2  23869  nrmhmph  23919  ptcmplem5  24181  restutop  24362  blin2  24554  met2ndci  24647  zdis  24942  reconnlem2  24953  cnheibor  25082  lebnum  25091  nmoleub2lem  25241  nmoleub2lem3  25242  nmoleub2lem2  25243  nmoleub3  25246  nmhmcn  25247  minveclem4  25559  ovolicc2lem5  25648  ioorcl  25704  ig1peu  26300  taylfvallem1  26485  tayl0  26490  ppisval  27233  ppinprm  27281  chtnprm  27283  chtleppi  27339  pclogsum  27344  chpchtsum  27348  chpub  27349  chebbnd1lem1  27598  chtppilimlem1  27602  rplogsum  27656  tglnpt4  28889  perpcom  28951  perpneq  28952  ragperp  28955  lnincplng  29023  perpprlng  29152  tocyc01  33378  cyc3evpm  33410  cycpmgcl  33413  cycpmconjslem2  33415  cyc3conja  33417  mxidlirred  33699  dflringlem3  33730  dflring4  33732  rprmirredb  33766  pidufd  33777  1arithufdlem4  33781  exsslsb  33931  lbsdiflsp0  33960  esum2d  34427  ispisys2  34487  sigapisys  34489  sigapildsyslem  34495  sigapildsys  34496  eulerpartlemgvv  34710  tgoldbachgt  34994  weiunfrlem  36863  weiunfr  36866  dfttc4  36929  fvineqsneq  37945  pibt2  37950  limclner  46256  fourierdlem49  46760  iinfconstbas  49728  ffthoppf  49827  thincciso  50115  termcterm2  50176  termcciso  50178  termccisoeu  50179  termfucterm  50206  uobeqterm  50208