MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elin Unicode version

Theorem elin 3522
Description: Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
elin  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )

Proof of Theorem elin
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elex 2956 . 2  |-  ( A  e.  ( B  i^i  C )  ->  A  e.  _V )
2 elex 2956 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32adantl 453 . 2  |-  ( ( A  e.  B  /\  A  e.  C )  ->  A  e.  _V )
4 eleq1 2495 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2495 . . . 4  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
64, 5anbi12d 692 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  x  e.  C
)  <->  ( A  e.  B  /\  A  e.  C ) ) )
7 df-in 3319 . . 3  |-  ( B  i^i  C )  =  { x  |  ( x  e.  B  /\  x  e.  C ) }
86, 7elab2g 3076 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) ) )
91, 3, 8pm5.21nii 343 1  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    = wceq 1652    e. wcel 1725   _Vcvv 2948    i^i cin 3311
This theorem is referenced by:  elin2  3523  elin3  3524  incom  3525  ineqri  3526  ineq1  3527  inass  3543  inss1  3553  ssin  3555  ssrin  3558  dfss4  3567  difin  3570  indi  3579  undi  3580  unineq  3583  indifdir  3589  difin2  3595  inrab2  3606  inelcm  3674  difin0ss  3686  inssdif0  3687  inundif  3698  uniin  4027  intun  4074  intpr  4075  elrint  4083  iunin2  4147  iinin2  4153  elriin  4155  disjor  4188  disjiun  4194  brin  4251  trin  4304  inex1  4336  inuni  4354  wefrc  4568  ordtri3or  4605  ordpwsuc  4786  inopab  4996  inxp  4998  dmin  5068  opelres  5142  intasym  5240  asymref  5241  dminss  5277  imainss  5278  inimasn  5280  ssrnres  5300  cnvresima  5350  dfco2a  5361  2elresin  5547  respreima  5850  isomin  6048  isoini  6049  offval  6303  tfrlem5  6632  erdisj  6943  uniinqs  6975  mapval2  7034  ixpin  7078  boxriin  7095  disjen  7255  ssenen  7272  onfin2  7289  elfpw  7399  unifpw  7400  f1opwfi  7401  fissuni  7402  fipreima  7403  elfir  7411  inelfi  7414  fiin  7418  inf3lem2  7573  cantnfcl  7611  epfrs  7656  cp  7804  bnd2  7806  tskwe  7826  infpwfidom  7898  infpwfien  7932  dfac5lem1  7993  dfac5lem5  7997  dfac5  7998  kmlem3  8021  kmlem14  8032  kmlem15  8033  ackbij2lem1  8088  ackbij1lem3  8091  ackbij1lem4  8092  ackbij1lem6  8094  ackbij1lem11  8099  fin23lem24  8191  fin23lem26  8194  isfin1-3  8255  fpwwe2lem12  8505  fpwwe  8510  canthnumlem  8512  pwxpndom2  8529  ingru  8679  gruina  8682  grur1  8684  axgroth4  8696  grothprim  8698  ixxdisj  10920  icodisj  11011  fzdisj  11067  uzdisj  11107  fzouzdisj  11157  fz1isolem  11698  limsupgle  12259  ello12  12298  elo12  12309  lo1resb  12346  rlimresb  12347  o1resb  12348  lo1eq  12350  rlimeq  12351  fsumsplit  12521  sumsplit  12540  fsum2dlem  12542  explecnv  12632  bitsmod  12936  saddisjlem  12964  sadadd  12967  sadass  12971  smuval2  12982  smupval  12988  smueqlem  12990  smumul  12993  prmreclem5  13276  prmrec  13278  4sqlem12  13312  vdwmc  13334  strfv2d  13487  submre  13818  submrc  13841  isacs2  13866  acsfn  13872  coffth  14121  catcoppccl  14251  catcfuccl  14252  catcxpccl  14292  isdrs2  14384  fpwipodrs  14578  psss  14634  subgacs  14963  nsgacs  14964  resscntz  15118  sylow2a  15241  lsmmod  15295  lsmdisj  15301  lsmdisj2  15302  subgdisj1  15311  frgpnabllem1  15472  gsumzsplit  15517  dmdprdd  15548  dprdfeq0  15568  dprdres  15574  subgdmdprd  15580  dprdcntz2  15584  dprddisj2  15585  dprd2da  15588  dmdprdsplit2lem  15591  ablfacrp  15612  pgpfac1lem3a  15622  pgpfac1lem3  15623  pgpfaclem1  15627  isrhm  15812  subsubrg2  15883  lssacs  16031  lspdisj  16185  lspdisjb  16186  isassa  16363  aspval  16375  aspid  16377  aspval2  16393  mplind  16550  zlpirlem1  16756  zlpirlem3  16758  dfprm2  16762  ocvin  16889  unocv  16895  iunocv  16896  obselocv  16943  isbasis2g  17001  baspartn  17007  tgval2  17009  bastg  17019  tgcl  17022  ppttop  17059  epttop  17061  clsval2  17102  ssntr  17110  isopn3  17118  ntreq0  17129  isclo  17139  restbas  17210  restntr  17234  restlp  17235  cnpresti  17340  cnprest  17341  cnprest2  17342  lmss  17350  haust1  17404  nrmsep3  17407  isnrm2  17410  lmmo  17432  cmpcovf  17442  fincmp  17444  0cmp  17445  discmp  17449  cmpsublem  17450  cmpsub  17451  uncmp  17454  hauscmplem  17457  bwth  17461  iscon2  17465  conclo  17466  dfcon2  17470  iunconlem  17478  uncon  17480  is1stc2  17493  1stcrest  17504  1stcelcls  17512  llyi  17525  nllyi  17526  llynlly  17528  subislly  17532  restnlly  17533  restlly  17534  islly2  17535  llyrest  17536  nllyrest  17537  llyidm  17539  nllyidm  17540  hausllycmp  17545  cldllycmp  17546  lly1stc  17547  dislly  17548  llycmpkgen2  17570  1stckgenlem  17573  txcnp  17640  txcnmpt  17644  txlly  17656  txnlly  17657  txtube  17660  txcmplem1  17661  txcmplem2  17662  hausdiag  17665  xkococnlem  17679  basqtop  17731  tgqtop  17732  kqcldsat  17753  ptcmpfi  17833  isfbas2  17855  isfil2  17876  infil  17883  fbasfip  17888  elfg  17891  filcon  17903  rnelfmlem  17972  rnelfm  17973  fmfnfmlem2  17975  fmfnfmlem4  17977  fmfnfm  17978  flimrest  18003  hauspwpwf1  18007  fclsrest  18044  alexsubALTlem2  18067  alexsubALTlem3  18068  alexsubALTlem4  18069  alexsubALT  18070  ptcmp  18077  istmd  18092  istgp  18095  tgpconcompss  18131  tsmssubm  18160  tsmssplit  18169  istrg  18181  istdrg  18183  istlm  18202  ustfilxp  18230  utoptop  18252  utop3cls  18269  bldisj  18416  blin  18439  blin2  18447  blres  18449  lpbl  18521  metrest  18542  restmetu  18605  isngp  18631  isnlm  18699  isnmhm  18768  tgioo  18815  xrtgioo  18825  xrsmopn  18831  zdis  18835  icccmplem1  18841  icccmplem2  18842  reconnlem2  18846  xrge0tsms  18853  icoopnst  18952  iocopnst  18953  cnheibor  18968  cnllycmp  18969  bndth  18971  iscph  19121  cphsqrcl  19135  tchcph  19182  cfilfcls  19215  cmetcaulem  19229  cmetss  19255  isbn  19279  cldcss2  19331  hlhil  19332  ovolfcl  19351  ovollb2lem  19372  ovolctb  19374  ovolshftlem1  19393  ovolscalem1  19397  ovolicc1  19400  ovolicc2lem2  19402  ovolicc2lem4  19404  ovolicc2lem5  19405  ovolicc2  19406  shftmbl  19421  volfiniun  19429  ioombl1lem1  19440  ioorf  19453  ioorcl  19457  dyadf  19471  vitalilem2  19489  vitali  19493  mbfmax  19529  mbfimaopnlem  19535  mbfaddlem  19540  mbfadd  19541  mbfsub  19542  i1faddlem  19573  i1fmullem  19574  i1fres  19585  itg1climres  19594  mbfi1fseqlem4  19598  mbfmul  19606  itg2splitlem  19628  itg2split  19629  itgresr  19658  bddmulibl  19718  ellimc2  19752  ellimc3  19754  limcun  19770  dvreslem  19784  dvres2lem  19785  dvaddbr  19812  dvmulbr  19813  dvne0  19883  lhop1lem  19885  lhop  19888  dvcnvrelem2  19890  itgsubstlem  19920  ig1peu  20082  ig1pval3  20085  aaliou2  20245  aaliou2b  20246  tayl0  20266  pilem1  20355  rlimcnp2  20793  xrlimcnp  20795  fsumharmonic  20838  ppisval  20874  ppisval2  20875  ppinprm  20923  chtnprm  20925  prmorcht  20949  fsumvma2  20986  pclogsum  20987  vmasum  20988  chpchtsum  20991  chpub  20992  2sqlem7  21142  chebbnd1lem1  21151  rpvmasum2  21194  issubgo  21879  isexid2  21901  smgrpismgm  21908  smgrpisass  21909  issmgrp  21910  mndoissmgrp  21915  mndoisexid  21916  mndomgmid  21918  ismndo  21919  rngo1cl  22005  minvecolem1  22364  minvecolem4a  22367  minvecolem4b  22368  minvecolem4  22370  h2hcau  22470  axhcompl-zf  22489  hhcmpl  22690  hhcms  22693  ocin  22786  ocnel  22788  shuni  22790  shmodsi  22879  pjhthlem2  22882  omlsilem  22892  pjoc1i  22921  spansnm0i  23140  nonbooli  23141  5oalem1  23144  5oalem2  23145  5oalem4  23147  5oalem5  23148  5oalem7  23150  3oalem2  23153  3oalem3  23154  pjssmii  23171  mayete3i  23218  mayete3iOLD  23219  nmcopex  23520  nmcoplb  23521  lncnopbd  23528  nmcfnex  23544  nmcfnlb  23545  riesz4  23555  riesz1  23556  riesz2  23557  cnlnadjlem3  23560  cnlnadjlem5  23562  cnlnadjlem9  23566  cnlnadjeu  23569  rnbra  23598  pjimai  23667  pjclem4a  23689  pjclem4  23690  pj3lem1  23697  pj3si  23698  jpi  23761  sumdmdii  23906  sumdmdlem  23909  sumdmdlem2  23910  cdjreui  23923  cdj3lem1  23925  disjorf  24009  ofpreima  24069  1stpreima  24083  2ndpreima  24084  iocinioc2  24130  ssnnssfz  24136  xrge0tsmsd  24211  kerunit  24249  cnre2csqima  24297  pnfneige0  24324  lmxrge0  24325  qqhucn  24364  esum0  24432  gsumesum  24439  esumcst  24443  esumpcvgval  24456  esumcvg  24464  sigainb  24507  measvuni  24556  cnllyscon  24920  rellyscon  24926  cvmsss2  24949  cvmcov2  24950  cvmopnlem  24953  fprod2dlem  25293  dfres3  25371  dfon2lem4  25397  predel  25438  wfrlem5  25515  frrlem5  25540  ellimits  25705  dfom5b  25707  brapply  25733  brcap  25735  dfrdg4  25745  tfrqfree  25746  onsucconi  26135  onintopsscon  26138  onsucsuccmpi  26141  limsucncmpi  26143  onint1  26147  mblfinlem  26190  mbfposadd  26200  itg2gt0cn  26206  finminlem  26258  comppfsc  26324  neibastop2lem  26326  neibastop2  26327  neifg  26337  tailfb  26343  inixp  26367  0totbnd  26419  sstotbnd3  26422  blbnd  26433  ssbnd  26434  heibor1lem  26455  heibor1  26456  heiborlem1  26457  heiborlem6  26462  heiborlem8  26464  heibor  26467  exidresid  26491  isfld2  26552  prtlem14  26660  elrfi  26685  elrfirn  26686  cmpfiiin  26688  mrefg2  26698  fz1eqin  26764  fnwe2lem2  27063  dfac11  27075  kelac1  27076  kelac2lem  27077  dfac21  27079  islmodfg  27082  islssfg2  27084  islssfgi  27085  filnm  27107  lnr2i  27235  lpirlnr  27236  hbtlem6  27248  hbt  27249  acsfn1p  27422  subrgacs  27423  sdrgacs  27424  cntzsdrg  27425  stoweidlem39  27702  stoweidlem44  27707  stoweidlem50  27713  stoweidlem57  27720  eldmressn  27898  afvres  27950  frgrancvvdeqlem4  28280  frgrancvvdeqlem7  28283  frgrancvvdeqlemA  28284  frgrancvvdeqlemC  28286  onfrALTlem2  28487  onfrALTlem2VD  28855  bnj521  28958  bnj1153  29018  bnj1172  29224  bnj1173  29225  bnj1174  29226  bnj1279  29241  lshpdisj  29624  lkrin  29801  ishlat1  29989  pmodlem1  30482  pmodlem2  30483  pclfinN  30536  pclcmpatN  30537  osumcllem4N  30595  pexmidlem1N  30606  dihmeetlem1N  31927  dihglblem5apreN  31928  dihmeetlem4preN  31943  dihmeetlem13N  31956  dochnel2  32029  lcdlss  32256  mapd1o  32285  mapdunirnN  32287  baerlem3lem2  32347  baerlem5alem2  32348  baerlem5blem2  32349  hdmaprnlem9N  32497
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319
  Copyright terms: Public domain W3C validator