Theorem elinel2 4143

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3889

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897

This theorem is referenced by:  elin2d  4146  nel2nelin  4149  eldmeldmressn  5985  onfr  6357  partfun  6640  fvcofneq  7040  offres  7930  fsplitfpar  8062  ressuppss  8127  frrlem4  8233  frrlem11  8240  frrlem12  8241  smores3  8287  erdisj  8695  dffi2  9330  r0weon  9928  fodomfi2  9976  ackbij1lem6  10140  ackbij1lem9  10143  ackbij1lem10  10144  ackbij1lem11  10145  ackbij1lem18  10152  isfin1-3  10302  dedekindle  11304  uzdisj  13545  nn0disj  13592  rlimres  15514  lo1res  15515  ackbijnn  15787  bitsinv2  16406  bitsf1ocnv  16407  smueqlem  16453  prmrec  16887  isstruct2  17113  isacs2  17613  isdrs2  18266  isacs3lem  18502  subrngpropd  20539  subrgpropd  20579  rnghmsubcsetclem2  20603  rhmsubcsetclem2  20632  rhmsubcrngclem2  20638  sralmod  21177  basdif0  22931  clsval2  23028  mreclatdemoBAD  23074  restfpw  23157  fincmp  23371  discmp  23376  uncmp  23381  cmpfi  23386  bwth  23388  iunconn  23406  1stcrest  23431  infil  23841  alexsublem  24022  alexsubALTlem3  24027  tsmsfbas  24106  tsmsgsum  24117  tsmssubm  24121  tsmsres  24122  tsmsf1o  24123  tsmsmhm  24124  tsmsadd  24125  tsmsxplem1  24131  tsmsxp  24133  blres  24409  reconnlem2  24806  xrge0tsms  24813  ncvsge0  25133  cphsscph  25231  cfilres  25276  ioombl1lem4  25541  mbfadd  25641  mbfsub  25642  mbfmul  25706  itg2cnlem2  25742  bddmulibl  25819  ellimc2  25857  fsumvma2  27194  vmasum  27196  chpchtsum  27199  chebbnd1lem1  27449  dirith2  27508  uhgrspansubgrlem  29376  disjin2  32675  xrge0tsmsd  33152  prsdm  34077  prsrn  34078  pibt2  37750  heicant  37993  mndoisexid  38207  eqvreldisj  39036  eldisjsim2  39273  fiinfi  44021  ismnushort  44749  restuni3  45569  disjinfi  45643  inmap  45659  iocopn  45971  icoopn  45976  icomnfinre  46003  uzinico  46010  islpcn  46088  lptre2pt  46089  limcresiooub  46091  limcresioolb  46092  limclner  46100  limsupmnflem  46169  limsupresxr  46215  liminfresxr  46216  liminfvalxr  46232  icccncfext  46336  stoweidlem39  46488  stoweidlem50  46499  stoweidlem57  46506  fourierdlem32  46588  fourierdlem33  46589  fourierdlem48  46603  fourierdlem49  46604  fourierdlem71  46626  fourierdlem80  46635  qndenserrnbllem  46743  sge0rnre  46813  sge0z  46824  sge0tsms  46829  sge0cl  46830  sge0f1o  46831  sge0fsum  46836  sge0sup  46840  sge0rnbnd  46842  sge0ltfirp  46849  sge0resplit  46855  sge0le  46856  sge0split  46858  sge0iunmptlemre  46864  sge0ltfirpmpt2  46875  sge0isum  46876  sge0xaddlem1  46882  sge0xaddlem2  46883  sge0pnffsumgt  46891  sge0gtfsumgt  46892  sge0uzfsumgt  46893  sge0seq  46895  sge0reuz  46896  meadjiunlem  46914  caragendifcl  46963  omeiunltfirp  46968  carageniuncllem2  46971  caratheodorylem2  46976  hspmbllem2  47076  pimiooltgt  47159  pimdecfgtioc  47164  pimincfltioc  47165  pimdecfgtioo  47166  pimincfltioo  47167  sssmf  47187  smfaddlem1  47212  smfaddlem2  47213  smfadd  47214  mbfpsssmf  47232  smfmullem4  47243  smfmul  47244  smfdiv  47246  smfsuplem1  47260  smfliminflem  47279  fmtno4prm  48053