Theorem elinel2 4155

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ∩ cin 3905

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913

This theorem is used by:  elin2d  4158  nel2nelin  4161  eldmeldmressn  6026  onfr  6404  partfun  6686  fvcofneq  7092  offres  7986  fsplitfpar  8119  ressuppss  8185  frrlem4  8292  frrlem11  8299  frrlem12  8300  smores3  8346  erdisj  8758  dffi2  9390  r0weon  10012  fodomfi2  10060  ackbij1lem6  10223  ackbij1lem9  10226  ackbij1lem10  10227  ackbij1lem11  10228  ackbij1lem18  10235  isfin1-3  10385  dedekindle  11391  uzdisj  13644  nn0disj  13691  rlimres  15635  lo1res  15636  ackbijnn  15907  bitsinv2  16525  bitsf1ocnv  16526  smueqlem  16572  prmrec  17006  isstruct2  17233  isacs2  17733  isdrs2  18386  isacs3lem  18622  subrngpropd  20719  subrgpropd  20759  rnghmsubcsetclem2  20783  rhmsubcsetclem2  20812  rhmsubcrngclem2  20818  sralmod  21360  basdif0  23162  clsval2  23259  mreclatdemoBAD  23305  restfpw  23388  fincmp  23602  discmp  23607  uncmp  23612  cmpfi  23617  bwth  23619  iunconn  23637  1stcrest  23662  infil  24073  alexsublem  24254  alexsubALTlem3  24259  tsmsfbas  24338  tsmsgsum  24349  tsmssubm  24353  tsmsres  24354  tsmsf1o  24355  tsmsmhm  24356  tsmsadd  24357  tsmsxplem1  24363  tsmsxp  24365  blres  24641  reconnlem2  25038  xrge0tsms  25045  ncvsge0  25365  cphsscph  25463  cfilres  25508  ioombl1lem4  25773  mbfadd  25873  mbfsub  25874  mbfmul  25938  itg2cnlem2  25974  bddmulibl  26051  ellimc2  26089  fsumvma2  27431  vmasum  27433  chpchtsum  27436  chebbnd1lem1  27686  dirith2  27745  uhgrspansubgrlem  29700  disjin2  33005  xrge0tsmsd  33459  prsdm  34370  prsrn  34371  pibt2  38122  heicant  38365  mndoisexid  38580  eqvreldisj  39407  eldisjsim2  39644  fiinfi  44359  ismnushort  45071  restuni3  45896  disjinfi  45970  inmap  45985  iocopn  46296  icoopn  46301  icomnfinre  46328  uzinico  46335  islpcn  46413  lptre2pt  46414  limcresiooub  46416  limcresioolb  46417  limclner  46425  limsupmnflem  46494  limsupresxr  46540  liminfresxr  46541  liminfvalxr  46557  icccncfext  46661  stoweidlem39  46813  stoweidlem50  46824  stoweidlem57  46831  fourierdlem32  46913  fourierdlem33  46914  fourierdlem48  46928  fourierdlem49  46929  fourierdlem71  46951  fourierdlem80  46960  qndenserrnbllem  47068  sge0rnre  47138  sge0z  47149  sge0tsms  47154  sge0cl  47155  sge0f1o  47156  sge0fsum  47161  sge0sup  47165  sge0rnbnd  47167  sge0ltfirp  47174  sge0resplit  47180  sge0le  47181  sge0split  47183  sge0iunmptlemre  47189  sge0ltfirpmpt2  47200  sge0isum  47201  sge0xaddlem1  47207  sge0xaddlem2  47208  sge0pnffsumgt  47216  sge0gtfsumgt  47217  sge0uzfsumgt  47218  sge0seq  47220  sge0reuz  47221  meadjiunlem  47239  caragendifcl  47288  omeiunltfirp  47293  carageniuncllem2  47296  caratheodorylem2  47301  hspmbllem2  47401  pimiooltgt  47484  pimdecfgtioc  47489  pimincfltioc  47490  pimdecfgtioo  47491  pimincfltioo  47492  sssmf  47512  smfaddlem1  47537  smfaddlem2  47538  smfadd  47539  mbfpsssmf  47557  smfmullem4  47568  smfmul  47569  smfdiv  47571  smfsuplem1  47585  smfliminflem  47604  fmtno4prm  48387