Theorem elin1d 4170

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924

This theorem is referenced by:  ordtypelem3  9480  ordtypelem4  9481  ordtypelem7  9484  infpwfien  10022  ttukeylem6  10474  fpwwe2lem11  10601  explecnv  15838  smuval2  16459  submrc  17596  coffth  17907  catcbascl  18081  acsfiindd  18519  frgpnabllem2  19811  ablfac2  20028  idomcringd  20643  2idllidld  21171  zringlpirlem2  21380  mplind  21984  neiptoptop  23025  restbas  23052  subbascn  23148  cnconn  23316  clsconn  23324  conncompclo  23329  cldllycmp  23389  llycmpkgen2  23444  1stckgenlem  23447  txcls  23498  txcnp  23514  ptcnplem  23515  xkopt  23549  txconn  23583  basqtop  23605  tgqtop  23606  kqnrmlem1  23637  kqnrmlem2  23638  nrmhmph  23688  ptcmplem5  23950  restutop  24132  blin2  24324  met2ndci  24417  zdis  24712  reconnlem2  24723  cnheibor  24861  lebnum  24870  nmoleub2lem  25021  nmoleub2lem3  25022  nmoleub2lem2  25023  nmoleub3  25026  nmhmcn  25027  minveclem4  25339  ovolicc2lem5  25429  ioorcl  25485  ig1peu  26087  taylfvallem1  26271  tayl0  26276  ppisval  27021  ppinprm  27069  chtnprm  27071  chtleppi  27128  pclogsum  27133  chpchtsum  27137  chpub  27138  chebbnd1lem1  27387  chtppilimlem1  27391  rplogsum  27445  perpcom  28647  perpneq  28648  ragperp  28651  tocyc01  33082  cyc3evpm  33114  cycpmgcl  33117  cycpmconjslem2  33119  cyc3conja  33121  idomrcanOLD  33239  unitpidl1  33402  ssdifidlprm  33436  mxidlirredi  33449  mxidlirred  33450  rprmirredb  33510  pidufd  33521  1arithufdlem4  33525  exsslsb  33599  lbsdiflsp0  33629  esum2d  34090  ispisys2  34150  sigapisys  34152  sigapildsyslem  34158  sigapildsys  34159  eulerpartlemgvv  34374  tgoldbachgt  34661  weiunfrlem  36459  weiunfr  36462  fvineqsneq  37407  pibt2  37412  limclner  45656  iinfconstbas  49059  ffthoppf  49158  thincciso  49446  termcterm2  49507  termcciso  49509  termccisoeu  49510  termfucterm  49537  uobeqterm  49539