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

Theorem elin 3532
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 2966 . 2  |-  ( A  e.  ( B  i^i  C )  ->  A  e.  _V )
2 elex 2966 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32adantl 454 . 2  |-  ( ( A  e.  B  /\  A  e.  C )  ->  A  e.  _V )
4 eleq1 2498 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2498 . . . 4  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
64, 5anbi12d 693 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  x  e.  C
)  <->  ( A  e.  B  /\  A  e.  C ) ) )
7 df-in 3329 . . 3  |-  ( B  i^i  C )  =  { x  |  ( x  e.  B  /\  x  e.  C ) }
86, 7elab2g 3086 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) ) )
91, 3, 8pm5.21nii 344 1  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   _Vcvv 2958    i^i cin 3321
This theorem is referenced by:  elin2  3533  elin3  3534  incom  3535  ineqri  3536  ineq1  3537  inass  3553  inss1  3563  ssin  3565  ssrin  3568  dfss4  3577  difin  3580  indi  3589  undi  3590  unineq  3593  indifdir  3599  difin2  3605  inrab2  3616  inelcm  3684  difin0ss  3696  inssdif0  3697  inundif  3708  uniin  4037  intun  4084  intpr  4085  elrint  4093  iunin2  4157  iinin2  4163  elriin  4166  disjor  4199  disjiun  4205  brin  4262  trin  4315  inex1  4347  inuni  4365  wefrc  4579  ordtri3or  4616  ordpwsuc  4798  inopab  5008  inxp  5010  dmin  5080  opelres  5154  intasym  5252  asymref  5253  dminss  5289  imainss  5290  inimasn  5292  ssrnres  5312  cnvresima  5362  dfco2a  5373  2elresin  5559  respreima  5862  isomin  6060  isoini  6061  offval  6315  tfrlem5  6644  erdisj  6955  uniinqs  6987  mapval2  7046  ixpin  7090  boxriin  7107  disjen  7267  ssenen  7284  onfin2  7301  elfpw  7411  unifpw  7412  f1opwfi  7413  fissuni  7414  fipreima  7415  elfir  7423  inelfi  7426  fiin  7430  inf3lem2  7587  cantnfcl  7625  epfrs  7670  cp  7820  bnd2  7822  tskwe  7842  infpwfidom  7914  infpwfien  7948  dfac5lem1  8009  dfac5lem5  8013  dfac5  8014  kmlem3  8037  kmlem14  8048  kmlem15  8049  ackbij2lem1  8104  ackbij1lem3  8107  ackbij1lem4  8108  ackbij1lem6  8110  ackbij1lem11  8115  fin23lem24  8207  fin23lem26  8210  isfin1-3  8271  fpwwe2lem12  8521  fpwwe  8526  canthnumlem  8528  pwxpndom2  8545  ingru  8695  gruina  8698  grur1  8700  axgroth4  8712  grothprim  8714  ixxdisj  10936  icodisj  11027  fzdisj  11083  uzdisj  11124  fzouzdisj  11174  fz1isolem  11715  limsupgle  12276  ello12  12315  elo12  12326  lo1resb  12363  rlimresb  12364  o1resb  12365  lo1eq  12367  rlimeq  12368  fsumsplit  12538  sumsplit  12557  fsum2dlem  12559  explecnv  12649  bitsmod  12953  saddisjlem  12981  sadadd  12984  sadass  12988  smuval2  12999  smupval  13005  smueqlem  13007  smumul  13010  prmreclem5  13293  prmrec  13295  4sqlem12  13329  vdwmc  13351  strfv2d  13504  submre  13835  submrc  13858  isacs2  13883  acsfn  13889  coffth  14138  catcoppccl  14268  catcfuccl  14269  catcxpccl  14309  isdrs2  14401  fpwipodrs  14595  psss  14651  subgacs  14980  nsgacs  14981  resscntz  15135  sylow2a  15258  lsmmod  15312  lsmdisj  15318  lsmdisj2  15319  subgdisj1  15328  frgpnabllem1  15489  gsumzsplit  15534  dmdprdd  15565  dprdfeq0  15585  dprdres  15591  subgdmdprd  15597  dprdcntz2  15601  dprddisj2  15602  dprd2da  15605  dmdprdsplit2lem  15608  ablfacrp  15629  pgpfac1lem3a  15639  pgpfac1lem3  15640  pgpfaclem1  15644  isrhm  15829  subsubrg2  15900  lssacs  16048  lspdisj  16202  lspdisjb  16203  isassa  16380  aspval  16392  aspid  16394  aspval2  16410  mplind  16567  zlpirlem1  16773  zlpirlem3  16775  dfprm2  16779  ocvin  16906  unocv  16912  iunocv  16913  obselocv  16960  isbasis2g  17018  baspartn  17024  tgval2  17026  bastg  17036  tgcl  17039  ppttop  17076  epttop  17078  clsval2  17119  ssntr  17127  isopn3  17135  ntreq0  17146  isclo  17156  restbas  17227  restntr  17251  restlp  17252  cnpresti  17357  cnprest  17358  cnprest2  17359  lmss  17367  haust1  17421  nrmsep3  17424  isnrm2  17427  lmmo  17449  cmpcovf  17459  fincmp  17461  0cmp  17462  discmp  17466  cmpsublem  17467  cmpsub  17468  uncmp  17471  hauscmplem  17474  bwth  17478  iscon2  17482  conclo  17483  dfcon2  17487  iunconlem  17495  uncon  17497  is1stc2  17510  1stcrest  17521  1stcelcls  17529  llyi  17542  nllyi  17543  llynlly  17545  subislly  17549  restnlly  17550  restlly  17551  islly2  17552  llyrest  17553  nllyrest  17554  llyidm  17556  nllyidm  17557  hausllycmp  17562  cldllycmp  17563  lly1stc  17564  dislly  17565  llycmpkgen2  17587  1stckgenlem  17590  txcnp  17657  txcnmpt  17661  txlly  17673  txnlly  17674  txtube  17677  txcmplem1  17678  txcmplem2  17679  hausdiag  17682  xkococnlem  17696  basqtop  17748  tgqtop  17749  kqcldsat  17770  ptcmpfi  17850  isfbas2  17872  isfil2  17893  infil  17900  fbasfip  17905  elfg  17908  filcon  17920  rnelfmlem  17989  rnelfm  17990  fmfnfmlem2  17992  fmfnfmlem4  17994  fmfnfm  17995  flimrest  18020  hauspwpwf1  18024  fclsrest  18061  alexsubALTlem2  18084  alexsubALTlem3  18085  alexsubALTlem4  18086  alexsubALT  18087  ptcmp  18094  istmd  18109  istgp  18112  tgpconcompss  18148  tsmssubm  18177  tsmssplit  18186  istrg  18198  istdrg  18200  istlm  18219  ustfilxp  18247  utoptop  18269  utop3cls  18286  bldisj  18433  blin  18456  blin2  18464  blres  18466  lpbl  18538  metrest  18559  restmetu  18622  isngp  18648  isnlm  18716  isnmhm  18785  tgioo  18832  xrtgioo  18842  xrsmopn  18848  zdis  18852  icccmplem1  18858  icccmplem2  18859  reconnlem2  18863  xrge0tsms  18870  icoopnst  18969  iocopnst  18970  cnheibor  18985  cnllycmp  18986  bndth  18988  iscph  19138  cphsqrcl  19152  tchcph  19199  cfilfcls  19232  cmetcaulem  19246  cmetss  19272  isbn  19296  cldcss2  19348  hlhil  19349  ovolfcl  19368  ovollb2lem  19389  ovolctb  19391  ovolshftlem1  19410  ovolscalem1  19414  ovolicc1  19417  ovolicc2lem2  19419  ovolicc2lem4  19421  ovolicc2lem5  19422  ovolicc2  19423  shftmbl  19438  volfiniun  19446  ioombl1lem1  19457  ioorf  19470  ioorcl  19474  dyadf  19488  vitalilem2  19506  vitali  19510  mbfmax  19544  mbfimaopnlem  19550  mbfaddlem  19555  mbfadd  19556  mbfsub  19557  i1faddlem  19588  i1fmullem  19589  i1fres  19600  itg1climres  19609  mbfi1fseqlem4  19613  mbfmul  19621  itg2splitlem  19643  itg2split  19644  itgresr  19673  bddmulibl  19733  ellimc2  19769  ellimc3  19771  limcun  19787  dvreslem  19801  dvres2lem  19802  dvaddbr  19829  dvmulbr  19830  dvne0  19900  lhop1lem  19902  lhop  19905  dvcnvrelem2  19907  itgsubstlem  19937  ig1peu  20099  ig1pval3  20102  aaliou2  20262  aaliou2b  20263  tayl0  20283  pilem1  20372  rlimcnp2  20810  xrlimcnp  20812  fsumharmonic  20855  ppisval  20891  ppisval2  20892  ppinprm  20940  chtnprm  20942  prmorcht  20966  fsumvma2  21003  pclogsum  21004  vmasum  21005  chpchtsum  21008  chpub  21009  2sqlem7  21159  chebbnd1lem1  21168  rpvmasum2  21211  issubgo  21896  isexid2  21918  smgrpismgm  21925  smgrpisass  21926  issmgrp  21927  mndoissmgrp  21932  mndoisexid  21933  mndomgmid  21935  ismndo  21936  rngo1cl  22022  minvecolem1  22381  minvecolem4a  22384  minvecolem4b  22385  minvecolem4  22387  h2hcau  22487  axhcompl-zf  22506  hhcmpl  22707  hhcms  22710  ocin  22803  ocnel  22805  shuni  22807  shmodsi  22896  pjhthlem2  22899  omlsilem  22909  pjoc1i  22938  spansnm0i  23157  nonbooli  23158  5oalem1  23161  5oalem2  23162  5oalem4  23164  5oalem5  23165  5oalem7  23167  3oalem2  23170  3oalem3  23171  pjssmii  23188  mayete3i  23235  mayete3iOLD  23236  nmcopex  23537  nmcoplb  23538  lncnopbd  23545  nmcfnex  23561  nmcfnlb  23562  riesz4  23572  riesz1  23573  riesz2  23574  cnlnadjlem3  23577  cnlnadjlem5  23579  cnlnadjlem9  23583  cnlnadjeu  23586  rnbra  23615  pjimai  23684  pjclem4a  23706  pjclem4  23707  pj3lem1  23714  pj3si  23715  jpi  23778  sumdmdii  23923  sumdmdlem  23926  sumdmdlem2  23927  cdjreui  23940  cdj3lem1  23942  disjorf  24026  ofpreima  24086  1stpreima  24100  2ndpreima  24101  iocinioc2  24147  ssnnssfz  24153  xrge0tsmsd  24228  kerunit  24266  cnre2csqima  24314  pnfneige0  24341  lmxrge0  24342  qqhucn  24381  esum0  24449  gsumesum  24456  esumcst  24460  esumpcvgval  24473  esumcvg  24481  sigainb  24524  measvuni  24573  cnllyscon  24937  rellyscon  24943  cvmsss2  24966  cvmcov2  24967  cvmopnlem  24970  fprod2dlem  25309  dfres3  25387  elima4  25409  dfon2lem4  25418  predel  25463  wfrlem5  25547  frrlem5  25591  ellimits  25760  dfom5b  25762  brapply  25788  brcap  25790  dfrdg4  25800  tfrqfree  25801  onsucconi  26192  onintopsscon  26195  onsucsuccmpi  26198  limsucncmpi  26200  onint1  26204  mblfinlem2  26256  mbfposadd  26266  itg2gt0cn  26274  finminlem  26335  comppfsc  26401  neibastop2lem  26403  neibastop2  26404  neifg  26414  tailfb  26420  inixp  26444  0totbnd  26496  sstotbnd3  26499  blbnd  26510  ssbnd  26511  heibor1lem  26532  heibor1  26533  heiborlem1  26534  heiborlem6  26539  heiborlem8  26541  heibor  26544  exidresid  26568  isfld2  26629  prtlem14  26737  elrfi  26762  elrfirn  26763  cmpfiiin  26765  mrefg2  26775  fz1eqin  26841  fnwe2lem2  27140  dfac11  27151  kelac1  27152  kelac2lem  27153  dfac21  27155  islmodfg  27158  islssfg2  27160  islssfgi  27161  filnm  27183  lnr2i  27311  lpirlnr  27312  hbtlem6  27324  hbt  27325  acsfn1p  27498  subrgacs  27499  sdrgacs  27500  cntzsdrg  27501  stoweidlem39  27778  stoweidlem44  27783  stoweidlem50  27789  stoweidlem57  27796  eldmressn  27974  afvres  28026  frgrancvvdeqlem4  28496  frgrancvvdeqlem7  28499  frgrancvvdeqlemA  28500  frgrancvvdeqlemC  28502  onfrALTlem2  28706  onfrALTlem2VD  29075  bnj521  29178  bnj1153  29238  bnj1172  29444  bnj1173  29445  bnj1174  29446  bnj1279  29461  lshpdisj  29859  lkrin  30036  ishlat1  30224  pmodlem1  30717  pmodlem2  30718  pclfinN  30771  pclcmpatN  30772  osumcllem4N  30830  pexmidlem1N  30841  dihmeetlem1N  32162  dihglblem5apreN  32163  dihmeetlem4preN  32178  dihmeetlem13N  32191  dochnel2  32264  lcdlss  32491  mapd1o  32520  mapdunirnN  32522  baerlem3lem2  32582  baerlem5alem2  32583  baerlem5blem2  32584  hdmaprnlem9N  32732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329
  Copyright terms: Public domain W3C validator