Theorem elin2d 4194

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
elin2d	⊢ (𝜑 → 𝑋 ∈ 𝐵)

Proof of Theorem elin2d

Step	Hyp	Ref	Expression
1		elin1d.1	. 2 ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))
2		elinel2 4191	. 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → 𝑋 ∈ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝑋 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2098   ∩ cin 3942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-v 3470  df-in 3950

This theorem is referenced by:  f1opwfi  9355  elfiun  9424  ordtypelem3  9514  infpwfien  10056  ttukeylem6  10508  fpwwe2lem11  10635  explecnv  15815  bitsinv1  16388  smuval2  16428  firest  17385  sscres  17777  funcres2c  17861  coffth  17896  rescfth  17897  catcoppccl  18077  catcoppcclOLD  18078  catcfuccl  18079  catcfucclOLD  18080  catcxpccl  18169  catcxpcclOLD  18170  psssdm2  18544  sylow2a  19537  frgpnabllem2  19792  sralmod  21041  2idlridld  21110  zringlpirlem3  21347  mplind  21969  neiptoptop  22986  restbas  23013  ordtrest  23057  subbascn  23109  lmss  23153  cnconn  23277  clsconn  23285  conncompclo  23290  subislly  23336  cldllycmp  23350  1stckgenlem  23408  txcls  23459  txcnp  23475  txtube  23495  txcmplem1  23496  txkgen  23507  xkopt  23510  xkococnlem  23514  txconn  23544  basqtop  23566  tgqtop  23567  kqnrmlem1  23598  kqnrmlem2  23599  nrmhmph  23649  uzrest  23752  alexsubALTlem3  23904  ptcmplem2  23908  tsmslem1  23984  tsmsxplem1  24008  tsmsxplem2  24009  tsmsxp  24010  blin2  24286  met2ndci  24382  zdis  24683  reconnlem2  24694  reconn  24695  xrge0gsumle  24700  cnheibor  24832  lebnum  24841  nmoleub2lem3  24993  nmoleub3  24997  caussi  25176  minveclem4b  25310  minveclem4  25311  ovolfcl  25346  ovolfioo  25347  ovolficc  25348  ovolficcss  25349  ovolfsval  25350  ovoliunlem1  25382  ovolicc2lem4  25400  ovolicc2lem5  25401  uniiccdif  25458  uniioovol  25459  uniiccvol  25460  uniioombllem2a  25462  uniioombllem3a  25464  uniioombllem4  25466  uniioombllem5  25467  uniioombllem6  25468  vitalilem2  25489  vitalilem4  25491  ig1peu  26060  taylfvallem1  26242  tayl0  26247  ppisval  26987  chtf  26991  efchtcl  26994  chtge0  26995  ppinprm  27035  chtprm  27036  chtnprm  27037  chtwordi  27039  chtdif  27041  efchtdvds  27042  chtlepsi  27090  chtleppi  27094  pclogsum  27099  chpval2  27102  chpchtsum  27103  chpub  27104  chebbnd1lem1  27353  chtppilimlem1  27357  rplogsumlem2  27369  perpneq  28469  ragperp  28472  tocyc01  32781  cyc3evpm  32813  cycpmconjslem2  32818  cyc3conja  32820  idomdomd  32878  mxidlirred  33094  ressdeg1  33150  lbsdiflsp0  33229  irngss  33270  esum2d  33621  ispisys2  33681  sigapisys  33683  sigapildsyslem  33689  sigapildsys  33690  sseqf  33921  tgoldbachgt  34204  bnj1172  34541  mhpind  41704  ismnushort  43617  cnrefiisplem  45098  hoiqssbllem3  45893  smflimlem3  46042