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

Theorem elin 3434
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 2872 . 2  |-  ( A  e.  ( B  i^i  C )  ->  A  e.  _V )
2 elex 2872 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32adantl 452 . 2  |-  ( ( A  e.  B  /\  A  e.  C )  ->  A  e.  _V )
4 eleq1 2418 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2418 . . . 4  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
64, 5anbi12d 691 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  x  e.  C
)  <->  ( A  e.  B  /\  A  e.  C ) ) )
7 df-in 3235 . . 3  |-  ( B  i^i  C )  =  { x  |  ( x  e.  B  /\  x  e.  C ) }
86, 7elab2g 2992 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) ) )
91, 3, 8pm5.21nii 342 1  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    = wceq 1642    e. wcel 1710   _Vcvv 2864    i^i cin 3227
This theorem is referenced by:  elin2  3435  elin3  3436  incom  3437  ineqri  3438  ineq1  3439  inass  3455  inss1  3465  ssin  3467  ssrin  3470  dfss4  3479  difin  3482  indi  3491  undi  3492  unineq  3495  indifdir  3501  difin2  3506  inrab2  3517  inelcm  3585  difin0ss  3596  inssdif0  3597  inundif  3608  uniin  3928  intun  3975  intpr  3976  elrint  3984  iunin2  4047  iinin2  4053  elriin  4055  disjor  4088  disjiun  4094  brin  4151  trin  4204  inex1  4236  inuni  4254  wefrc  4469  ordtri3or  4506  ordpwsuc  4688  inopab  4898  inxp  4900  dmin  4968  opelres  5042  intasym  5140  asymref  5141  dminss  5177  imainss  5178  ssrnres  5198  cnvresima  5244  dfco2a  5255  2elresin  5437  respreima  5737  isomin  5921  isoini  5922  offval  6172  tfrlem5  6483  erdisj  6794  uniinqs  6826  mapval2  6885  ixpin  6929  boxriin  6946  disjen  7106  ssenen  7123  onfin2  7140  elfpw  7247  unifpw  7248  f1opwfi  7249  fissuni  7250  fipreima  7251  elfir  7259  fiin  7265  inf3lem2  7420  cantnfcl  7458  epfrs  7503  cp  7651  bnd2  7653  tskwe  7673  infpwfidom  7745  infpwfien  7779  dfac5lem1  7840  dfac5lem5  7844  dfac5  7845  kmlem3  7868  kmlem14  7879  kmlem15  7880  ackbij2lem1  7935  ackbij1lem3  7938  ackbij1lem4  7939  ackbij1lem6  7941  ackbij1lem11  7946  fin23lem24  8038  fin23lem26  8041  isfin1-3  8102  fpwwe2lem12  8353  fpwwe  8358  canthnumlem  8360  pwxpndom2  8377  ingru  8527  gruina  8530  grur1  8532  axgroth4  8544  grothprim  8546  ixxdisj  10763  icodisj  10853  fzdisj  10909  uzdisj  10948  fzouzdisj  10994  fz1isolem  11495  limsupgle  12047  ello12  12086  elo12  12097  lo1resb  12134  rlimresb  12135  o1resb  12136  lo1eq  12138  rlimeq  12139  fsumsplit  12309  sumsplit  12328  fsum2dlem  12330  explecnv  12420  bitsmod  12724  saddisjlem  12752  sadadd  12755  sadass  12759  smuval2  12770  smupval  12776  smueqlem  12778  smumul  12781  prmreclem5  13064  prmrec  13066  4sqlem12  13100  vdwmc  13122  strfv2d  13275  submre  13606  submrc  13629  isacs2  13654  acsfn  13660  coffth  13909  catcoppccl  14039  catcfuccl  14040  catcxpccl  14080  isdrs2  14172  fpwipodrs  14366  psss  14422  subgacs  14751  nsgacs  14752  resscntz  14906  sylow2a  15029  lsmmod  15083  lsmdisj  15089  lsmdisj2  15090  subgdisj1  15099  frgpnabllem1  15260  gsumzsplit  15305  dmdprdd  15336  dprdfeq0  15356  dprdres  15362  subgdmdprd  15368  dprdcntz2  15372  dprddisj2  15373  dprd2da  15376  dmdprdsplit2lem  15379  ablfacrp  15400  pgpfac1lem3a  15410  pgpfac1lem3  15411  pgpfaclem1  15415  isrhm  15600  subsubrg2  15671  lssacs  15823  lspdisj  15977  lspdisjb  15978  isassa  16155  aspval  16167  aspid  16169  aspval2  16185  mplind  16342  zlpirlem1  16547  zlpirlem3  16549  dfprm2  16553  ocvin  16680  unocv  16686  iunocv  16687  obselocv  16734  isbasis2g  16792  baspartn  16798  tgval2  16800  bastg  16810  tgcl  16813  ppttop  16850  epttop  16852  clsval2  16893  ssntr  16901  isopn3  16909  ntreq0  16920  isclo  16930  restbas  16995  restntr  17018  restlp  17019  cnpresti  17122  cnprest  17123  cnprest2  17124  lmss  17132  haust1  17186  nrmsep3  17189  isnrm2  17192  lmmo  17214  cmpcovf  17224  fincmp  17226  0cmp  17227  discmp  17231  cmpsublem  17232  cmpsub  17233  uncmp  17236  hauscmplem  17239  iscon2  17246  conclo  17247  dfcon2  17251  iunconlem  17259  uncon  17261  is1stc2  17274  1stcrest  17285  1stcelcls  17293  llyi  17306  nllyi  17307  llynlly  17309  subislly  17313  restnlly  17314  restlly  17315  islly2  17316  llyrest  17317  nllyrest  17318  llyidm  17320  nllyidm  17321  hausllycmp  17326  cldllycmp  17327  lly1stc  17328  dislly  17329  llycmpkgen2  17351  1stckgenlem  17354  txcnp  17420  txcnmpt  17424  txlly  17436  txnlly  17437  txtube  17440  txcmplem1  17441  txcmplem2  17442  hausdiag  17445  xkococnlem  17459  basqtop  17508  tgqtop  17509  kqcldsat  17530  ptcmpfi  17610  isfbas2  17632  isfil2  17653  infil  17660  fbasfip  17665  elfg  17668  filcon  17680  rnelfmlem  17749  rnelfm  17750  fmfnfmlem2  17752  fmfnfmlem4  17754  fmfnfm  17755  flimrest  17780  hauspwpwf1  17784  fclsrest  17821  alexsubALTlem2  17844  alexsubALTlem3  17845  alexsubALTlem4  17846  alexsubALT  17847  ptcmp  17854  istmd  17859  istgp  17862  tgpconcompss  17898  tsmssubm  17927  tsmssplit  17936  istrg  17948  istdrg  17950  istlm  17969  bldisj  18057  blin  18072  blin2  18077  blres  18079  lpbl  18151  metrest  18172  isngp  18220  isnlm  18288  isnmhm  18357  tgioo  18404  xrtgioo  18414  xrsmopn  18420  zdis  18424  icccmplem1  18430  icccmplem2  18431  reconnlem2  18435  xrge0tsms  18442  icoopnst  18541  iocopnst  18542  cnheibor  18557  cnllycmp  18558  bndth  18560  iscph  18710  cphsqrcl  18724  tchcph  18771  cfilfcls  18804  cmetcaulem  18818  cmetss  18844  isbn  18864  cldcss2  18910  hlhil  18911  ovolfcl  18930  ovollb2lem  18951  ovolctb  18953  ovolshftlem1  18972  ovolscalem1  18976  ovolicc1  18979  ovolicc2lem2  18981  ovolicc2lem4  18983  ovolicc2lem5  18984  ovolicc2  18985  shftmbl  19000  volfiniun  19008  ioombl1lem1  19019  ioorf  19032  ioorcl  19036  dyadf  19050  vitalilem2  19068  vitali  19072  mbfmax  19108  mbfimaopnlem  19114  mbfaddlem  19119  mbfadd  19120  mbfsub  19121  i1faddlem  19152  i1fmullem  19153  i1fres  19164  itg1climres  19173  mbfi1fseqlem4  19177  mbfmul  19185  itg2splitlem  19207  itg2split  19208  itgresr  19237  bddmulibl  19297  ellimc2  19331  ellimc3  19333  limcun  19349  dvreslem  19363  dvres2lem  19364  dvaddbr  19391  dvmulbr  19392  dvne0  19462  lhop1lem  19464  lhop  19467  dvcnvrelem2  19469  itgsubstlem  19499  ig1peu  19661  ig1pval3  19664  aaliou2  19824  aaliou2b  19825  tayl0  19845  pilem1  19934  rlimcnp2  20372  xrlimcnp  20374  fsumharmonic  20417  ppisval  20453  ppisval2  20454  ppinprm  20502  chtnprm  20504  prmorcht  20528  fsumvma2  20565  pclogsum  20566  vmasum  20567  chpchtsum  20570  chpub  20571  2sqlem7  20721  chebbnd1lem1  20730  rpvmasum2  20773  issubgo  21082  isexid2  21104  smgrpismgm  21111  smgrpisass  21112  issmgrp  21113  mndoissmgrp  21118  mndoisexid  21119  mndomgmid  21121  ismndo  21122  rngo1cl  21208  minvecolem1  21567  minvecolem4a  21570  minvecolem4b  21571  minvecolem4  21573  h2hcau  21673  axhcompl-zf  21692  hhcmpl  21893  hhcms  21896  ocin  21989  ocnel  21991  shuni  21993  shmodsi  22082  pjhthlem2  22085  omlsilem  22095  pjoc1i  22124  spansnm0i  22343  nonbooli  22344  5oalem1  22347  5oalem2  22348  5oalem4  22350  5oalem5  22351  5oalem7  22353  3oalem2  22356  3oalem3  22357  pjssmii  22374  mayete3i  22421  mayete3iOLD  22422  nmcopex  22723  nmcoplb  22724  lncnopbd  22731  nmcfnex  22747  nmcfnlb  22748  riesz4  22758  riesz1  22759  riesz2  22760  cnlnadjlem3  22763  cnlnadjlem5  22765  cnlnadjlem9  22769  cnlnadjeu  22772  rnbra  22801  pjimai  22870  pjclem4a  22892  pjclem4  22893  pj3lem1  22900  pj3si  22901  jpi  22964  sumdmdii  23109  sumdmdlem  23112  sumdmdlem2  23113  cdjreui  23126  cdj3lem1  23128  disjorf  23220  inimasn  23235  1stpreima  23299  2ndpreima  23300  inelfi  23318  iocinioc2  23344  ssnnssfz  23350  xrge0tsmsd  23415  kerunit  23427  cnre2csqima  23465  pnfneige0  23492  lmxrge0  23493  ustfilxp  23518  utoptop  23538  restmetu  23615  indf1ofs  23689  esum0  23710  gsumesum  23717  esumcst  23721  esumpcvgval  23734  esumcvg  23742  sigainb  23785  measvuni  23832  cnllyscon  24180  rellyscon  24186  cvmsss2  24209  cvmcov2  24210  cvmopnlem  24213  dfres3  24674  dfon2lem4  24700  predel  24741  wfrlem5  24818  frrlem5  24843  ellimits  25008  dfom5b  25010  brapply  25035  brcap  25037  dfrdg4  25047  tfrqfree  25048  onsucconi  25435  onintopsscon  25438  onsucsuccmpi  25441  limsucncmpi  25443  onint1  25447  itg2gt0cn  25495  cnvresimaOLD  25550  finminlem  25555  comppfsc  25631  neibastop2lem  25633  neibastop2  25634  neifg  25644  tailfb  25650  inixp  25723  0totbnd  25820  sstotbnd3  25823  blbnd  25834  ssbnd  25835  heibor1lem  25856  heibor1  25857  heiborlem1  25858  heiborlem6  25863  heiborlem8  25865  heibor  25868  exidresid  25892  isfld2  25953  prtlem14  26065  elrfi  26092  elrfirn  26093  cmpfiiin  26095  mrefg2  26105  fz1eqin  26171  fnwe2lem2  26471  dfac11  26483  kelac1  26484  kelac2lem  26485  dfac21  26487  islmodfg  26490  islssfg2  26492  islssfgi  26493  filnm  26515  lnr2i  26643  lpirlnr  26644  hbtlem6  26656  hbt  26657  acsfn1p  26830  subrgacs  26831  sdrgacs  26832  cntzsdrg  26833  stoweidlem39  27111  stoweidlem44  27116  stoweidlem50  27122  stoweidlem57  27129  eldmressn  27307  afvres  27360  frgrancvvdeqlem4  27866  frgrancvvdeqlem7  27869  frgrancvvdeqlemA  27870  frgrancvvdeqlemC  27872  onfrALTlem2  28056  onfrALTlem2VD  28427  bnj521  28527  bnj1153  28587  bnj1172  28793  bnj1173  28794  bnj1174  28795  bnj1279  28810  lshpdisj  29246  lkrin  29423  ishlat1  29611  pmodlem1  30104  pmodlem2  30105  pclfinN  30158  pclcmpatN  30159  osumcllem4N  30217  pexmidlem1N  30228  dihmeetlem1N  31549  dihglblem5apreN  31550  dihmeetlem4preN  31565  dihmeetlem13N  31578  dochnel2  31651  lcdlss  31878  mapd1o  31907  mapdunirnN  31909  baerlem3lem2  31969  baerlem5alem2  31970  baerlem5blem2  31971  hdmaprnlem9N  32119
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-in 3235
  Copyright terms: Public domain W3C validator