Theorem elin1d 4144

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3888

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896

This theorem is referenced by:  ordtypelem3  9435  ordtypelem4  9436  ordtypelem7  9439  infpwfien  9984  ttukeylem6  10436  fpwwe2lem11  10564  explecnv  15830  smuval2  16451  submrc  17594  coffth  17905  catcbascl  18079  acsfiindd  18519  frgpnabllem2  19849  ablfac2  20066  idomcringd  20704  2idllidld  21252  zringlpirlem2  21443  mplind  22048  neiptoptop  23096  restbas  23123  subbascn  23219  cnconn  23387  clsconn  23395  conncompclo  23400  cldllycmp  23460  llycmpkgen2  23515  1stckgenlem  23518  txcls  23569  txcnp  23585  ptcnplem  23586  xkopt  23620  txconn  23654  basqtop  23676  tgqtop  23677  kqnrmlem1  23708  kqnrmlem2  23709  nrmhmph  23759  ptcmplem5  24021  restutop  24202  blin2  24394  met2ndci  24487  zdis  24782  reconnlem2  24793  cnheibor  24922  lebnum  24931  nmoleub2lem  25081  nmoleub2lem3  25082  nmoleub2lem2  25083  nmoleub3  25086  nmhmcn  25087  minveclem4  25399  ovolicc2lem5  25488  ioorcl  25544  ig1peu  26140  taylfvallem1  26322  tayl0  26327  ppisval  27067  ppinprm  27115  chtnprm  27117  chtleppi  27173  pclogsum  27178  chpchtsum  27182  chpub  27183  chebbnd1lem1  27432  chtppilimlem1  27436  rplogsum  27490  perpcom  28781  perpneq  28782  ragperp  28785  tocyc01  33179  cyc3evpm  33211  cycpmgcl  33214  cycpmconjslem2  33216  cyc3conja  33218  idomrcanOLD  33343  unitpidl1  33484  ssdifidlprm  33518  mxidlirredi  33531  mxidlirred  33532  rprmirredb  33592  pidufd  33603  1arithufdlem4  33607  exsslsb  33741  lbsdiflsp0  33770  esum2d  34237  ispisys2  34297  sigapisys  34299  sigapildsyslem  34305  sigapildsys  34306  eulerpartlemgvv  34520  tgoldbachgt  34807  weiunfrlem  36646  weiunfr  36649  dfttc4  36712  fvineqsneq  37728  pibt2  37733  limclner  46079  iinfconstbas  49541  ffthoppf  49640  thincciso  49928  termcterm2  49989  termcciso  49991  termccisoeu  49992  termfucterm  50019  uobeqterm  50021