Theorem elinel2 4152

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 3915	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2	1	simprbi 496	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2113   ∩ cin 3898

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906

This theorem is referenced by:  elin2d  4155  nel2nelin  4158  eldmeldmressn  5982  onfr  6354  partfun  6637  fvcofneq  7036  offres  7925  fsplitfpar  8058  ressuppss  8123  frrlem4  8229  frrlem11  8236  frrlem12  8237  smores3  8283  erdisj  8690  dffi2  9324  r0weon  9920  fodomfi2  9968  ackbij1lem6  10132  ackbij1lem9  10135  ackbij1lem10  10136  ackbij1lem11  10137  ackbij1lem18  10144  isfin1-3  10294  dedekindle  11295  uzdisj  13511  nn0disj  13558  rlimres  15479  lo1res  15480  ackbijnn  15749  bitsinv2  16368  bitsf1ocnv  16369  smueqlem  16415  prmrec  16848  isstruct2  17074  isacs2  17574  isdrs2  18227  isacs3lem  18463  subrngpropd  20499  subrgpropd  20539  rnghmsubcsetclem2  20563  rhmsubcsetclem2  20592  rhmsubcrngclem2  20598  sralmod  21137  basdif0  22895  clsval2  22992  mreclatdemoBAD  23038  restfpw  23121  fincmp  23335  discmp  23340  uncmp  23345  cmpfi  23350  bwth  23352  iunconn  23370  1stcrest  23395  infil  23805  alexsublem  23986  alexsubALTlem3  23991  tsmsfbas  24070  tsmsgsum  24081  tsmssubm  24085  tsmsres  24086  tsmsf1o  24087  tsmsmhm  24088  tsmsadd  24089  tsmsxplem1  24095  tsmsxp  24097  blres  24373  reconnlem2  24770  xrge0tsms  24777  ncvsge0  25107  cphsscph  25205  cfilres  25250  ioombl1lem4  25516  mbfadd  25616  mbfsub  25617  mbfmul  25681  itg2cnlem2  25717  bddmulibl  25794  ellimc2  25832  fsumvma2  27179  vmasum  27181  chpchtsum  27184  chebbnd1lem1  27434  dirith2  27493  uhgrspansubgrlem  29312  disjin2  32611  xrge0tsmsd  33104  prsdm  34020  prsrn  34021  pibt2  37561  heicant  37795  mndoisexid  38009  eqvreldisj  38810  fiinfi  43756  ismnushort  44484  restuni3  45304  disjinfi  45378  inmap  45395  iocopn  45708  icoopn  45713  icomnfinre  45740  uzinico  45747  islpcn  45825  lptre2pt  45826  limcresiooub  45828  limcresioolb  45829  limclner  45837  limsupmnflem  45906  limsupresxr  45952  liminfresxr  45953  liminfvalxr  45969  icccncfext  46073  stoweidlem39  46225  stoweidlem50  46236  stoweidlem57  46243  fourierdlem32  46325  fourierdlem33  46326  fourierdlem48  46340  fourierdlem49  46341  fourierdlem71  46363  fourierdlem80  46372  qndenserrnbllem  46480  sge0rnre  46550  sge0z  46561  sge0tsms  46566  sge0cl  46567  sge0f1o  46568  sge0fsum  46573  sge0sup  46577  sge0rnbnd  46579  sge0ltfirp  46586  sge0resplit  46592  sge0le  46593  sge0split  46595  sge0iunmptlemre  46601  sge0ltfirpmpt2  46612  sge0isum  46613  sge0xaddlem1  46619  sge0xaddlem2  46620  sge0pnffsumgt  46628  sge0gtfsumgt  46629  sge0uzfsumgt  46630  sge0seq  46632  sge0reuz  46633  meadjiunlem  46651  caragendifcl  46700  omeiunltfirp  46705  carageniuncllem2  46708  caratheodorylem2  46713  hspmbllem2  46813  pimiooltgt  46896  pimdecfgtioc  46901  pimincfltioc  46902  pimdecfgtioo  46903  pimincfltioo  46904  sssmf  46924  smfaddlem1  46949  smfaddlem2  46950  smfadd  46951  mbfpsssmf  46969  smfmullem4  46980  smfmul  46981  smfdiv  46983  smfsuplem1  46997  smfliminflem  47016  fmtno4prm  47763