Theorem elinel2 4148

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 503	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906

This theorem is used by:  elin2d  4151  nel2nelin  4154  eldmeldmressn  6018  onfr  6397  partfun  6680  fvcofneq  7087  offres  7981  fsplitfpar  8116  ressuppss  8182  frrlem4  8289  frrlem11  8296  frrlem12  8297  smores3  8343  erdisj  8757  dffi2  9396  r0weon  10018  fodomfi2  10066  ackbij1lem6  10229  ackbij1lem9  10232  ackbij1lem10  10233  ackbij1lem11  10234  ackbij1lem18  10241  isfin1-3  10391  dedekindle  11401  uzdisj  13655  nn0disj  13702  rlimres  15648  lo1res  15649  ackbijnn  15920  bitsinv2  16536  bitsf1ocnv  16537  smueqlem  16583  prmrec  17017  isstruct2  17244  isacs2  17744  isdrs2  18397  isacs3lem  18633  subrngpropd  20733  subrgpropd  20773  rnghmsubcsetclem2  20797  rhmsubcsetclem2  20826  rhmsubcrngclem2  20832  sralmod  21374  basdif0  23181  clsval2  23278  mreclatdemoBAD  23324  restfpw  23407  fincmp  23621  discmp  23626  uncmp  23631  cmpfi  23636  bwth  23638  iunconn  23656  1stcrest  23681  infil  24092  alexsublem  24273  alexsubALTlem3  24278  tsmsfbas  24357  tsmsgsum  24368  tsmssubm  24372  tsmsres  24373  tsmsf1o  24374  tsmsmhm  24375  tsmsadd  24376  tsmsxplem1  24382  tsmsxp  24384  blres  24660  reconnlem2  25057  xrge0tsms  25064  ncvsge0  25384  cphsscph  25482  cfilres  25527  ioombl1lem4  25792  mbfadd  25892  mbfsub  25893  mbfmul  25957  itg2cnlem2  25993  bddmulibl  26069  ellimc2  26107  fsumvma2  27453  vmasum  27455  chpchtsum  27458  chebbnd1lem1  27708  dirith2  27767  uhgrspansubgrlem  29753  disjin2  33063  xrge0tsmsd  33516  prsdm  34427  prsrn  34428  pibt2  38174  heicant  38407  mndoisexid  38622  eqvreldisj  39449  eldisjsim2  39686  fiinfi  44416  ismnushort  45128  restuni3  45953  disjinfi  46027  inmap  46042  iocopn  46353  icoopn  46358  icomnfinre  46385  uzinico  46392  islpcn  46470  lptre2pt  46471  limcresiooub  46473  limcresioolb  46474  limclner  46482  limsupmnflem  46551  limsupresxr  46597  liminfresxr  46598  liminfvalxr  46614  icccncfext  46718  stoweidlem39  46870  stoweidlem50  46881  stoweidlem57  46888  fourierdlem32  46970  fourierdlem33  46971  fourierdlem48  46985  fourierdlem49  46986  fourierdlem71  47008  fourierdlem80  47017  qndenserrnbllem  47125  sge0rnre  47195  sge0z  47206  sge0tsms  47211  sge0cl  47212  sge0f1o  47213  sge0fsum  47218  sge0sup  47222  sge0rnbnd  47224  sge0ltfirp  47231  sge0resplit  47237  sge0le  47238  sge0split  47240  sge0iunmptlemre  47246  sge0ltfirpmpt2  47257  sge0isum  47258  sge0xaddlem1  47264  sge0xaddlem2  47265  sge0pnffsumgt  47273  sge0gtfsumgt  47274  sge0uzfsumgt  47275  sge0seq  47277  sge0reuz  47278  meadjiunlem  47296  caragendifcl  47345  omeiunltfirp  47350  carageniuncllem2  47353  caratheodorylem2  47358  hspmbllem2  47458  pimiooltgt  47541  pimdecfgtioc  47546  pimincfltioc  47547  pimdecfgtioo  47548  pimincfltioo  47549  sssmf  47569  smfaddlem1  47594  smfaddlem2  47595  smfadd  47596  mbfpsssmf  47614  smfmullem4  47625  smfmul  47626  smfdiv  47628  smfsuplem1  47642  smfliminflem  47661  fmtno4prm  48481