Theorem elinel2 4156

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

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

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 3444  df-in 3910

This theorem is referenced by:  elin2d  4159  nel2nelin  4162  eldmeldmressn  5992  onfr  6364  partfun  6647  fvcofneq  7047  offres  7937  fsplitfpar  8070  ressuppss  8135  frrlem4  8241  frrlem11  8248  frrlem12  8249  smores3  8295  erdisj  8703  dffi2  9338  r0weon  9934  fodomfi2  9982  ackbij1lem6  10146  ackbij1lem9  10149  ackbij1lem10  10150  ackbij1lem11  10151  ackbij1lem18  10158  isfin1-3  10308  dedekindle  11309  uzdisj  13525  nn0disj  13572  rlimres  15493  lo1res  15494  ackbijnn  15763  bitsinv2  16382  bitsf1ocnv  16383  smueqlem  16429  prmrec  16862  isstruct2  17088  isacs2  17588  isdrs2  18241  isacs3lem  18477  subrngpropd  20516  subrgpropd  20556  rnghmsubcsetclem2  20580  rhmsubcsetclem2  20609  rhmsubcrngclem2  20615  sralmod  21154  basdif0  22912  clsval2  23009  mreclatdemoBAD  23055  restfpw  23138  fincmp  23352  discmp  23357  uncmp  23362  cmpfi  23367  bwth  23369  iunconn  23387  1stcrest  23412  infil  23822  alexsublem  24003  alexsubALTlem3  24008  tsmsfbas  24087  tsmsgsum  24098  tsmssubm  24102  tsmsres  24103  tsmsf1o  24104  tsmsmhm  24105  tsmsadd  24106  tsmsxplem1  24112  tsmsxp  24114  blres  24390  reconnlem2  24787  xrge0tsms  24794  ncvsge0  25124  cphsscph  25222  cfilres  25267  ioombl1lem4  25533  mbfadd  25633  mbfsub  25634  mbfmul  25698  itg2cnlem2  25734  bddmulibl  25811  ellimc2  25849  fsumvma2  27196  vmasum  27198  chpchtsum  27201  chebbnd1lem1  27451  dirith2  27510  uhgrspansubgrlem  29379  disjin2  32678  xrge0tsmsd  33171  prsdm  34096  prsrn  34097  pibt2  37676  heicant  37910  mndoisexid  38124  eqvreldisj  38953  eldisjsim2  39190  fiinfi  43933  ismnushort  44661  restuni3  45481  disjinfi  45555  inmap  45571  iocopn  45884  icoopn  45889  icomnfinre  45916  uzinico  45923  islpcn  46001  lptre2pt  46002  limcresiooub  46004  limcresioolb  46005  limclner  46013  limsupmnflem  46082  limsupresxr  46128  liminfresxr  46129  liminfvalxr  46145  icccncfext  46249  stoweidlem39  46401  stoweidlem50  46412  stoweidlem57  46419  fourierdlem32  46501  fourierdlem33  46502  fourierdlem48  46516  fourierdlem49  46517  fourierdlem71  46539  fourierdlem80  46548  qndenserrnbllem  46656  sge0rnre  46726  sge0z  46737  sge0tsms  46742  sge0cl  46743  sge0f1o  46744  sge0fsum  46749  sge0sup  46753  sge0rnbnd  46755  sge0ltfirp  46762  sge0resplit  46768  sge0le  46769  sge0split  46771  sge0iunmptlemre  46777  sge0ltfirpmpt2  46788  sge0isum  46789  sge0xaddlem1  46795  sge0xaddlem2  46796  sge0pnffsumgt  46804  sge0gtfsumgt  46805  sge0uzfsumgt  46806  sge0seq  46808  sge0reuz  46809  meadjiunlem  46827  caragendifcl  46876  omeiunltfirp  46881  carageniuncllem2  46884  caratheodorylem2  46889  hspmbllem2  46989  pimiooltgt  47072  pimdecfgtioc  47077  pimincfltioc  47078  pimdecfgtioo  47079  pimincfltioo  47080  sssmf  47100  smfaddlem1  47125  smfaddlem2  47126  smfadd  47127  mbfpsssmf  47145  smfmullem4  47156  smfmul  47157  smfdiv  47159  smfsuplem1  47173  smfliminflem  47192  fmtno4prm  47939