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

Theorem elin 3788
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 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))

Proof of Theorem elin
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elex 3207 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3207 . . 3 (𝐴𝐶𝐴 ∈ V)
32adantl 482 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2687 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2687 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
64, 5anbi12d 746 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
7 df-in 3574 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
86, 7elab2g 3347 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
91, 3, 8pm5.21nii 368 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384   = wceq 1481  wcel 1988  Vcvv 3195  cin 3566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574
This theorem is referenced by:  elini  3789  elind  3790  elinel1  3791  elinel2  3792  elin2  3793  elin3  3796  incom  3797  ineqri  3798  ineq1  3799  inass  3815  ssin  3827  ssrin  3830  dfss4  3850  difin  3853  indi  3865  undi  3866  unineq  3869  indifdir  3875  difin2  3882  inrab2  3892  difin0ss  3937  inssdif0  3938  inelcm  4023  inundif  4037  elinsn  4236  uniin  4448  intun  4500  intpr  4501  elrint  4509  iunin2  4575  iinin2  4581  elriin  4584  disjor  4625  disjiun  4631  brin  4695  trin  4754  inex1  4790  inuni  4817  wefrc  5098  inopab  5241  inxp  5243  dmin  5321  opelres  5390  intasym  5499  asymref  5500  dminss  5535  imainss  5536  inimasn  5538  ssrnres  5560  cnvresima  5611  dfco2a  5623  ordtri3or  5743  2elresin  5990  respreima  6330  fvcofneq  6353  tpres  6451  isomin  6572  isoini  6573  offval  6889  ordpwsuc  7000  ressuppss  7299  wfrlem5  7404  erdisj  7779  uniinqs  7812  mapval2  7872  ixpin  7918  boxriin  7935  disjen  8102  ssenen  8119  onfin2  8137  elfpw  8253  fiin  8313  inf3lem2  8511  epfrs  8592  cp  8739  bnd2  8741  dfac5lem1  8931  dfac5lem5  8935  dfac5  8936  kmlem3  8959  kmlem14  8970  kmlem15  8971  fin23lem26  9132  isfin1-3  9193  pwxpndom2  9472  ingru  9622  gruina  9625  grur1  9627  axgroth4  9639  grothprim  9641  ixxdisj  12175  icodisj  12282  fzdisj  12353  uzdisj  12397  nn0disj  12439  fzouzdisj  12488  xpcogend  13694  cotr2g  13696  limsupgle  14189  ello12  14228  elo12  14239  lo1resb  14276  rlimresb  14277  o1resb  14278  lo1eq  14280  rlimeq  14281  fsumsplit  14452  sumsplit  14480  fsum2dlem  14482  explecnv  14578  fprod2dlem  14691  bitsmod  15139  saddisjlem  15167  sadadd  15170  sadass  15174  smuval2  15185  smupval  15191  smueqlem  15193  smumul  15196  isprm7  15401  prmreclem5  15605  prmrec  15607  4sqlem12  15641  vdwmc  15663  setsstruct2  15877  acsfn  16301  iszeroo  16633  iszeroi  16640  isdrs2  16920  fpwipodrs  17145  psss  17195  subgacs  17610  nsgacs  17611  resscntz  17745  gsmsymgreq  17833  sylow2a  18015  lsmmod  18069  lsmdisj2  18076  gsumzsplit  18308  subgdmdprd  18414  dprdcntz2  18418  dprddisj2  18419  pgpfac1lem3  18457  isrhm  18702  subsubrg2  18788  lssacs  18948  lspdisj  19106  lspdisjb  19107  isassa  19296  aspid  19311  aspval2  19328  dfprm2  19823  ocvin  19999  unocv  20005  iunocv  20006  obselocv  20053  pmatcoe1fsupp  20487  isbasis2g  20733  tgval2  20741  tgcl  20754  ppttop  20792  epttop  20794  clsval2  20835  ssntr  20843  ntreq0  20862  isclo  20872  restntr  20967  restlp  20968  cnpresti  21073  cnprest  21074  cnprest2  21075  lmss  21083  haust1  21137  nrmsep3  21140  isnrm2  21143  lmmo  21165  fincmp  21177  0cmp  21178  discmp  21182  cmpsublem  21183  cmpsub  21184  uncmp  21187  hauscmplem  21190  dfconn2  21203  iunconnlem  21211  unconn  21213  is1stc2  21226  1stcrest  21237  1stcelcls  21245  llyi  21258  nllyi  21259  subislly  21265  lly1stc  21280  comppfsc  21316  txcnp  21404  txcnmpt  21408  hausdiag  21429  kqcldsat  21517  ptcmpfi  21597  isfbas2  21620  isfil2  21641  fbasfip  21653  elfg  21656  filconn  21668  rnelfmlem  21737  rnelfm  21738  fmfnfmlem2  21740  fmfnfmlem4  21742  fmfnfm  21743  flimrest  21768  hauspwpwf1  21772  fclsrest  21809  alexsubALTlem2  21833  alexsubALTlem3  21834  alexsubALTlem4  21835  alexsubALT  21836  ptcmp  21843  istmd  21859  istgp  21862  tsmssubm  21927  tsmssplit  21936  istrg  21948  istdrg  21950  istlm  21969  ustfilxp  21997  utoptop  22019  utop3cls  22036  bldisj  22184  blin  22207  blin2  22215  blres  22217  lpbl  22289  metrest  22310  restmetu  22356  isngp  22381  isnlm  22460  isnmhm  22531  xrtgioo  22590  xrsmopn  22596  icccmplem2  22607  reconnlem2  22611  icoopnst  22719  iocopnst  22720  bndth  22738  cvsi  22911  cnstrcvs  22922  cncvs  22926  zclmncvs  22929  isncvsngp  22930  ncvsprp  22933  ncvsm1  22935  ncvsdif  22936  ncvspi  22937  ncvs1  22938  ncvspds  22942  iscph  22951  tchcph  23017  cfilfcls  23053  cmetcaulem  23067  cmetss  23094  isbn  23116  cldcss2  23194  hlhil  23195  ovolfcl  23216  ovolicc1  23265  ovolicc2lem2  23267  ovolicc2lem4  23269  ovolicc2lem5  23270  ovolicc2  23271  shftmbl  23287  volfiniun  23296  ioorf  23322  mbfmax  23397  mbfimaopnlem  23403  mbfaddlem  23408  mbfadd  23409  mbfsub  23410  i1faddlem  23441  i1fmullem  23442  i1fres  23453  itg1climres  23462  mbfi1fseqlem4  23466  mbfmul  23474  itg2splitlem  23496  itg2split  23497  itgresr  23526  bddmulibl  23586  ellimc2  23622  ellimc3  23624  limcun  23640  dvreslem  23654  dvne0  23755  itgsubstlem  23792  ig1pval3  23915  aaliou2  24076  aaliou2b  24077  pilem1  24186  rlimcnp2  24674  fsumharmonic  24719  ppisval2  24812  prmorcht  24885  fsumvma2  24920  pclogsum  24921  vmasum  24922  chpchtsum  24925  chpub  24926  chebbnd1lem1  25139  rpvmasum2  25182  tglineineq  25519  trlsegvdeg  27067  frgrncvvdeqlem7  27149  frgrncvvdeqlem9  27151  minvecolem1  27700  minvecolem4a  27703  minvecolem4b  27704  minvecolem4  27706  h2hcau  27806  axhcompl-zf  27825  hhcmpl  28027  hhcms  28030  ocin  28125  ocnel  28127  shmodsi  28218  pjhthlem2  28221  omlsilem  28231  pjoc1i  28260  spansnm0i  28479  nonbooli  28480  5oalem7  28489  3oalem3  28493  pjssmii  28510  mayete3i  28557  nmcopex  28858  nmcoplb  28859  lncnopbd  28866  nmcfnex  28882  nmcfnlb  28883  riesz4  28893  riesz1  28894  riesz2  28895  cnlnadjlem3  28898  cnlnadjlem5  28900  cnlnadjlem9  28904  cnlnadjeu  28907  rnbra  28936  pjimai  29005  pjclem4a  29027  pj3lem1  29035  jpi  29099  sumdmdii  29244  sumdmdlem  29247  sumdmdlem2  29248  cdjreui  29261  cdj3lem1  29263  iunin1f  29346  disjorf  29364  ofpreima  29439  1stpreima  29458  2ndpreima  29459  iocinioc2  29515  ssnnssfz  29523  isorng  29773  kerunit  29797  crefdf  29889  cmpcref  29891  cmppcmp  29899  pcmplfin  29901  cnre2csqima  29931  ordtconnlem1  29944  lmxrge0  29972  isrrext  30018  esum0  30085  esumcst  30099  esumpcvgval  30114  esumcvg  30122  measvuni  30251  eulerpartlemt0  30405  eulerpartlemr  30410  eulerpartlemgf  30415  eulerpartlemgs2  30416  eulerpartlemn  30417  sseqf  30428  fiblem  30434  oddprm2  30707  bnj521  30779  bnj1173  31044  bnj1174  31045  bnj1279  31060  dfres3  31624  elima4  31653  imaindm  31656  dfon2lem4  31665  frrlem5  31758  madeval2  31910  ellimits  31992  dfom5b  31994  brapply  32020  brcap  32022  dfrecs2  32032  dfrdg4  32033  finminlem  32287  neibastop2lem  32330  neibastop2  32331  neifg  32341  tailfb  32347  onsucconni  32411  onintopssconn  32414  onsucsuccmpi  32417  limsucncmpi  32419  onint1  32423  bj-inrab  32898  bj-restuni  33025  bj-eldiag  33062  bj-eldiag2  33063  bj-ccinftydisj  33071  taupilem3  33136  isbasisrelowllem1  33174  isbasisrelowllem2  33175  ptrest  33379  poimirlem29  33409  poimirlem30  33410  mblfinlem2  33418  mbfposadd  33428  itg2gt0cn  33436  dvasin  33467  inixp  33494  0totbnd  33543  sstotbnd3  33546  heibor1lem  33579  heibor1  33580  heiborlem6  33586  isexid2  33625  smgrpismgmOLD  33632  issmgrpOLD  33633  mndoissmgrpOLD  33638  ismndo  33642  exidresid  33649  rngo1cl  33709  isfld2  33775  prtlem14  33978  lshpdisj  34093  lkrin  34270  ishlat1  34458  pmodlem2  34952  pclfinN  35005  pclcmpatN  35006  osumcllem4N  35064  pexmidlem1N  35075  dihmeetlem1N  36398  dihglblem5apreN  36399  dihmeetlem4preN  36414  dihmeetlem13N  36427  dochnel2  36500  lcdlss  36727  mapd1o  36756  baerlem3lem2  36818  baerlem5alem2  36819  baerlem5blem2  36820  cmpfiiin  37079  mrefg2  37089  fz1eqin  37151  fnwe2lem2  37440  islmodfg  37458  islssfg2  37460  lnr2i  37505  acsfn1p  37588  subrgacs  37589  sdrgacs  37590  rp-fakeinunass  37680  fiinfi  37697  elinintab  37700  elinintrab  37702  elinlem  37723  cnvcnvintabd  37725  ndisj  37883  ntrneikb  38212  ntrneik3  38214  ntrneik13  38216  radcnvrat  38333  nzin  38337  onfrALTlem2  38581  onfrALTlem2VD  38945  inn0f  39062  nel2nelin  39158  iooabslt  39524  iccintsng  39552  lptioo2cn  39677  lptioo1cn  39678  cncfuni  39862  icccncfext  39863  stoweidlem44  40024  fourierdlem42  40129  fourierdlem80  40166  sge00  40356  eldmressn  40966  afvres  41015  31prm  41277  rnghmval2  41660  rnghmsubcsetclem1  41740  rngccatidALTV  41754  funcrngcsetcALT  41764  zrinitorngc  41765  zrtermorngc  41766  rhmsubcsetclem1  41786  rhmsubcrngclem1  41792  ringcbasbas  41799  funcringcsetcALTV2lem7  41807  ringccatidALTV  41817  ringcbasbasALTV  41823  funcringcsetclem7ALTV  41830  irinitoringc  41834  zrtermoringc  41835  srhmsubclem1  41838  fldhmsubc  41849  fldhmsubcALTV  41867  rhmsubcALTVlem3  41871  ssnn0ssfz  41892  elbigo2  42111
  Copyright terms: Public domain W3C validator