Theorem elinel2 4195

Description: Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
elinel2	⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)

Proof of Theorem elinel2

Step	Hyp	Ref	Expression
1		elin 3963	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2	1	simprbi 497	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2106   ∩ cin 3946

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954

This theorem is referenced by:  elin2d  4198  eldmeldmressn  6023  onfr  6400  partfun  6694  fvcofneq  7091  offres  7966  fsplitfpar  8100  ressuppss  8164  frrlem4  8270  frrlem11  8277  frrlem12  8278  wfrlem4OLD  8308  smores3  8349  erdisj  8751  dffi2  9414  r0weon  10003  fodomfi2  10051  ackbij1lem6  10216  ackbij1lem9  10219  ackbij1lem10  10220  ackbij1lem11  10221  ackbij1lem18  10228  isfin1-3  10377  dedekindle  11374  uzdisj  13570  nn0disj  13613  rlimres  15498  lo1res  15499  ackbijnn  15770  bitsinv2  16380  bitsf1ocnv  16381  smueqlem  16427  prmrec  16851  isstruct2  17078  isacs2  17593  isdrs2  18255  isacs3lem  18491  subrgpropd  20392  sralmod  20801  basdif0  22447  clsval2  22545  mreclatdemoBAD  22591  restfpw  22674  fincmp  22888  discmp  22893  uncmp  22898  cmpfi  22903  bwth  22905  iunconn  22923  1stcrest  22948  infil  23358  alexsublem  23539  alexsubALTlem3  23544  tsmsfbas  23623  tsmsgsum  23634  tsmssubm  23638  tsmsres  23639  tsmsf1o  23640  tsmsmhm  23641  tsmsadd  23642  tsmsxplem1  23648  tsmsxp  23650  blres  23928  reconnlem2  24334  xrge0tsms  24341  ncvsge0  24661  cphsscph  24759  cfilres  24804  ioombl1lem4  25069  mbfadd  25169  mbfsub  25170  mbfmul  25235  itg2cnlem2  25271  bddmulibl  25347  ellimc2  25385  fsumvma2  26706  vmasum  26708  chpchtsum  26711  chebbnd1lem1  26961  dirith2  27020  uhgrspansubgrlem  28536  disjin2  31805  xrge0tsmsd  32196  prsdm  32882  prsrn  32883  pibt2  36286  heicant  36511  mndoisexid  36725  eqvreldisj  37472  fiinfi  42309  ismnushort  43045  restuni3  43792  nel2nelin  43821  disjinfi  43876  inmap  43893  iocopn  44219  icoopn  44224  icomnfinre  44251  uzinico  44259  islpcn  44341  lptre2pt  44342  limcresiooub  44344  limcresioolb  44345  limclner  44353  limsupmnflem  44422  limsupresxr  44468  liminfresxr  44469  liminfvalxr  44485  icccncfext  44589  stoweidlem39  44741  stoweidlem50  44752  stoweidlem57  44759  fourierdlem32  44841  fourierdlem33  44842  fourierdlem48  44856  fourierdlem49  44857  fourierdlem71  44879  fourierdlem80  44888  qndenserrnbllem  44996  sge0rnre  45066  sge0z  45077  sge0tsms  45082  sge0cl  45083  sge0f1o  45084  sge0fsum  45089  sge0sup  45093  sge0rnbnd  45095  sge0ltfirp  45102  sge0resplit  45108  sge0le  45109  sge0split  45111  sge0iunmptlemre  45117  sge0ltfirpmpt2  45128  sge0isum  45129  sge0xaddlem1  45135  sge0xaddlem2  45136  sge0pnffsumgt  45144  sge0gtfsumgt  45145  sge0uzfsumgt  45146  sge0seq  45148  sge0reuz  45149  meadjiunlem  45167  caragendifcl  45216  omeiunltfirp  45221  carageniuncllem2  45224  caratheodorylem2  45229  hspmbllem2  45329  pimiooltgt  45412  pimdecfgtioc  45417  pimincfltioc  45418  pimdecfgtioo  45419  pimincfltioo  45420  sssmf  45440  smfaddlem1  45465  smfaddlem2  45466  smfadd  45467  mbfpsssmf  45485  smfmullem4  45496  smfmul  45497  smfdiv  45499  smfsuplem1  45513  smfliminflem  45532  fmtno4prm  46229  subrngpropd  46731  rnghmsubcsetclem2  46827  rhmsubcsetclem2  46873  rhmsubcrngclem2  46879