Theorem elinel2 4154

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

Syntax hints:   → wi 4   ∈ wcel 2142   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911

This theorem is referenced by:  elin2d  4157  nel2nelin  4160  eldmeldmressn  6011  onfr  6385  partfun  6668  fvcofneq  7074  offres  7964  fsplitfpar  8097  ressuppss  8163  frrlem4  8270  frrlem11  8277  frrlem12  8278  smores3  8324  erdisj  8736  dffi2  9369  r0weon  9968  fodomfi2  10016  ackbij1lem6  10180  ackbij1lem9  10183  ackbij1lem10  10184  ackbij1lem11  10185  ackbij1lem18  10192  isfin1-3  10343  dedekindle  11347  uzdisj  13602  nn0disj  13649  rlimres  15585  lo1res  15586  ackbijnn  15858  bitsinv2  16477  bitsf1ocnv  16478  smueqlem  16524  prmrec  16958  isstruct2  17185  isacs2  17685  isdrs2  18338  isacs3lem  18574  subrngpropd  20618  subrgpropd  20658  rnghmsubcsetclem2  20682  rhmsubcsetclem2  20711  rhmsubcrngclem2  20717  sralmod  21254  basdif0  23013  clsval2  23110  mreclatdemoBAD  23156  restfpw  23239  fincmp  23453  discmp  23458  uncmp  23463  cmpfi  23468  bwth  23470  iunconn  23488  1stcrest  23513  infil  23923  alexsublem  24104  alexsubALTlem3  24109  tsmsfbas  24188  tsmsgsum  24199  tsmssubm  24203  tsmsres  24204  tsmsf1o  24205  tsmsmhm  24206  tsmsadd  24207  tsmsxplem1  24213  tsmsxp  24215  blres  24491  reconnlem2  24888  xrge0tsms  24895  ncvsge0  25215  cphsscph  25313  cfilres  25358  ioombl1lem4  25623  mbfadd  25723  mbfsub  25724  mbfmul  25788  itg2cnlem2  25824  bddmulibl  25901  ellimc2  25939  fsumvma2  27278  vmasum  27280  chpchtsum  27283  chebbnd1lem1  27533  dirith2  27592  uhgrspansubgrlem  29491  disjin2  32787  xrge0tsmsd  33253  prsdm  34211  prsrn  34212  pibt2  37911  heicant  38154  mndoisexid  38368  eqvreldisj  39197  eldisjsim2  39434  fiinfi  44149  ismnushort  44877  restuni3  45696  disjinfi  45770  inmap  45785  iocopn  46096  icoopn  46101  icomnfinre  46128  uzinico  46135  islpcn  46213  lptre2pt  46214  limcresiooub  46216  limcresioolb  46217  limclner  46225  limsupmnflem  46294  limsupresxr  46340  liminfresxr  46341  liminfvalxr  46357  icccncfext  46461  stoweidlem39  46613  stoweidlem50  46624  stoweidlem57  46631  fourierdlem32  46713  fourierdlem33  46714  fourierdlem48  46728  fourierdlem49  46729  fourierdlem71  46751  fourierdlem80  46760  qndenserrnbllem  46868  sge0rnre  46938  sge0z  46949  sge0tsms  46954  sge0cl  46955  sge0f1o  46956  sge0fsum  46961  sge0sup  46965  sge0rnbnd  46967  sge0ltfirp  46974  sge0resplit  46980  sge0le  46981  sge0split  46983  sge0iunmptlemre  46989  sge0ltfirpmpt2  47000  sge0isum  47001  sge0xaddlem1  47007  sge0xaddlem2  47008  sge0pnffsumgt  47016  sge0gtfsumgt  47017  sge0uzfsumgt  47018  sge0seq  47020  sge0reuz  47021  meadjiunlem  47039  caragendifcl  47088  omeiunltfirp  47093  carageniuncllem2  47096  caratheodorylem2  47101  hspmbllem2  47201  pimiooltgt  47284  pimdecfgtioc  47289  pimincfltioc  47290  pimdecfgtioo  47291  pimincfltioo  47292  sssmf  47312  smfaddlem1  47337  smfaddlem2  47338  smfadd  47339  mbfpsssmf  47357  smfmullem4  47368  smfmul  47369  smfdiv  47371  smfsuplem1  47385  smfliminflem  47404  fmtno4prm  48184