Theorem elin1d 4151

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

Syntax hints:   → wi 4   ∈ wcel 2111   ∩ cin 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904

This theorem is referenced by:  ordtypelem3  9406  ordtypelem4  9407  ordtypelem7  9410  infpwfien  9953  ttukeylem6  10405  fpwwe2lem11  10532  explecnv  15772  smuval2  16393  submrc  17534  coffth  17845  catcbascl  18019  acsfiindd  18459  frgpnabllem2  19786  ablfac2  20003  idomcringd  20642  2idllidld  21191  zringlpirlem2  21400  mplind  22005  neiptoptop  23046  restbas  23073  subbascn  23169  cnconn  23337  clsconn  23345  conncompclo  23350  cldllycmp  23410  llycmpkgen2  23465  1stckgenlem  23468  txcls  23519  txcnp  23535  ptcnplem  23536  xkopt  23570  txconn  23604  basqtop  23626  tgqtop  23627  kqnrmlem1  23658  kqnrmlem2  23659  nrmhmph  23709  ptcmplem5  23971  restutop  24152  blin2  24344  met2ndci  24437  zdis  24732  reconnlem2  24743  cnheibor  24881  lebnum  24890  nmoleub2lem  25041  nmoleub2lem3  25042  nmoleub2lem2  25043  nmoleub3  25046  nmhmcn  25047  minveclem4  25359  ovolicc2lem5  25449  ioorcl  25505  ig1peu  26107  taylfvallem1  26291  tayl0  26296  ppisval  27041  ppinprm  27089  chtnprm  27091  chtleppi  27148  pclogsum  27153  chpchtsum  27157  chpub  27158  chebbnd1lem1  27407  chtppilimlem1  27411  rplogsum  27465  perpcom  28691  perpneq  28692  ragperp  28695  tocyc01  33087  cyc3evpm  33119  cycpmgcl  33122  cycpmconjslem2  33124  cyc3conja  33126  idomrcanOLD  33248  unitpidl1  33389  ssdifidlprm  33423  mxidlirredi  33436  mxidlirred  33437  rprmirredb  33497  pidufd  33508  1arithufdlem4  33512  exsslsb  33609  lbsdiflsp0  33639  esum2d  34106  ispisys2  34166  sigapisys  34168  sigapildsyslem  34174  sigapildsys  34175  eulerpartlemgvv  34389  tgoldbachgt  34676  weiunfrlem  36508  weiunfr  36511  fvineqsneq  37456  pibt2  37461  limclner  45759  iinfconstbas  49177  ffthoppf  49276  thincciso  49564  termcterm2  49625  termcciso  49627  termccisoeu  49628  termfucterm  49655  uobeqterm  49657