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

Theorem elin 3887
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 3431 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3431 . . 3 (𝐴𝐶𝐴 ∈ V)
32adantl 485 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2825 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2825 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
64, 5anbi12d 634 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
7 df-in 3878 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
86, 7elab2g 3594 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
91, 3, 8pm5.21nii 383 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399   = wceq 1543  wcel 2110  Vcvv 3413  cin 3870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3415  df-in 3878
This theorem is referenced by:  dfss2  3891  elini  4112  elind  4113  elinel1  4114  elinel2  4115  elin2  4116  elin3  4119  incomOLD  4121  ineqri  4124  inass  4139  ssin  4150  ssrin  4153  rexin  4159  dfss4  4178  difin  4181  indi  4193  undi  4194  unineq  4197  indifdi  4203  indifdirOLD  4205  difin2  4211  inrab2  4227  ndisj  4287  difin0ss  4288  inssdif0  4289  inelcm  4384  inundif  4398  elinsn  4631  uniin  4850  intun  4896  intprg  4897  intprOLD  4899  elrint  4907  iunin2  4984  iinin2  4991  elriin  4994  disjor  5038  disjiun  5045  brin  5110  trin  5176  inex1  5215  inuni  5241  wefrc  5550  inopab  5704  inxp  5706  dmin  5785  dfres3  5861  intasym  5985  asymref  5986  dminss  6021  imainss  6022  inimasn  6024  cnvresima  6098  dfco2a  6115  ordtri3or  6250  2elresin  6503  respreima  6891  fvcofneq  6917  tpres  7021  isomin  7151  isoini  7152  offval  7482  ordpwsuc  7599  ressuppss  7930  frrlem13  8044  fprlem1  8046  wfrlem5  8064  uniinqs  8484  mapval2  8558  ixpin  8609  boxriin  8626  disjen  8808  ssenen  8825  onfin2  8876  elfpw  8983  fiin  9043  inf3lem2  9249  epfrs  9352  cp  9512  dfac5lem1  9742  dfac5lem5  9746  dfac5  9747  kmlem3  9771  kmlem14  9782  kmlem15  9783  fin23lem26  9944  pwxpndom2  10284  ingru  10434  gruina  10437  grur1  10439  axgroth4  10451  grothprim  10453  ixxdisj  12955  icodisj  13069  fzdisj  13144  nn0disj  13233  fzouzdisj  13283  cotr2g  14544  limsupgle  15043  ello12  15082  elo12  15093  lo1resb  15130  rlimresb  15131  o1resb  15132  lo1eq  15134  rlimeq  15135  fsumsplit  15310  sumsplit  15337  fsum2dlem  15339  fprod2dlem  15547  bitsmod  16000  saddisjlem  16028  sadadd  16031  sadass  16035  smuval2  16046  smupval  16052  smueqlem  16054  smumul  16057  isprm7  16270  prmreclem5  16478  prmrec  16480  4sqlem12  16514  vdwmc  16536  setsstruct2  16732  acsfn  17167  iszeroo  17509  iszeroi  17520  fpwipodrs  18051  psss  18091  insubm  18250  subgacs  18582  nsgacs  18583  resscntz  18731  gsmsymgreq  18829  sylow2a  19013  lsmmod  19070  lsmdisj2  19077  gsumzsplit  19317  subgdmdprd  19426  dprdcntz2  19430  dprddisj2  19431  pgpfac1lem3  19469  isrhm  19746  subsubrg2  19832  acsfn1p  19848  subrgacs  19849  sdrgacs  19850  lssacs  20009  lspdisj  20167  lspdisjb  20168  dfprm2  20465  ocvin  20641  unocv  20647  iunocv  20648  obselocv  20695  isassa  20823  aspid  20839  aspval2  20863  pmatcoe1fsupp  21603  isbasis2g  21850  tgval2  21858  tgcl  21871  ppttop  21909  epttop  21911  ssntr  21960  ntreq0  21979  isclo  21989  restntr  22084  restlp  22085  cnpresti  22190  cnprest  22191  cnprest2  22192  lmss  22200  haust1  22254  nrmsep3  22257  isnrm2  22260  lmmo  22282  fincmp  22295  cmpsublem  22301  cmpsub  22302  uncmp  22305  hauscmplem  22308  dfconn2  22321  iunconnlem  22329  unconn  22331  is1stc2  22344  1stcrest  22355  1stcelcls  22363  llyi  22376  nllyi  22377  subislly  22383  lly1stc  22398  txcnp  22522  txcnmpt  22526  hausdiag  22547  kqcldsat  22635  isfbas2  22737  isfil2  22758  fbasfip  22770  elfg  22773  filconn  22785  rnelfmlem  22854  rnelfm  22855  fmfnfmlem2  22857  fmfnfmlem4  22859  fmfnfm  22860  flimrest  22885  hauspwpwf1  22889  fclsrest  22926  alexsubALTlem2  22950  alexsubALTlem3  22951  alexsubALTlem4  22952  alexsubALT  22953  istmd  22976  istgp  22979  tsmssubm  23045  tsmssplit  23054  istrg  23066  istdrg  23068  istlm  23087  ustfilxp  23115  utoptop  23137  utop3cls  23154  bldisj  23301  blin  23324  blres  23334  lpbl  23406  metrest  23427  restmetu  23473  isngp  23499  isnlm  23578  isnmhm  23649  xrtgioo  23708  xrsmopn  23714  icccmplem2  23725  reconnlem2  23729  icoopnst  23841  iocopnst  23842  bndth  23860  zclmncvs  24050  isncvsngp  24051  ncvsprp  24054  ncvsm1  24056  ncvsdif  24057  ncvspi  24058  ncvs1  24059  ncvspds  24063  iscph  24072  tcphcph  24139  cfilfcls  24176  cmetcaulem  24190  isbn  24240  cldcss2  24344  hlhil  24345  ovolfcl  24368  ovolicc2lem2  24420  ovolicc2  24424  shftmbl  24440  volfiniun  24449  mbfmax  24551  mbfimaopnlem  24557  mbfaddlem  24562  i1faddlem  24595  i1fmullem  24596  i1fres  24608  itg1climres  24617  mbfi1fseqlem4  24621  itg2splitlem  24651  itg2split  24652  itgresr  24681  ellimc2  24779  ellimc3  24781  limcun  24797  dvreslem  24811  dvne0  24913  itgsubstlem  24950  ig1pval3  25077  aaliou2  25238  aaliou2b  25239  pilem1  25348  rlimcnp2  25854  fsumharmonic  25899  ppisval2  25992  prmorcht  26065  fsumvma2  26100  pclogsum  26101  vmasum  26102  chpchtsum  26105  chpub  26106  rpvmasum2  26398  tglineineq  26739  trlsegvdeg  28315  frgrncvvdeqlem7  28393  frgrncvvdeqlem9  28395  minvecolem1  28960  minvecolem4a  28963  minvecolem4b  28964  minvecolem4  28966  h2hcau  29065  axhcompl-zf  29084  hhcmpl  29286  hhcms  29289  ocin  29382  ocnel  29384  shmodsi  29475  pjhthlem2  29478  omlsilem  29488  pjoc1i  29517  spansnm0i  29736  nonbooli  29737  5oalem7  29746  3oalem3  29750  pjssmii  29767  mayete3i  29814  nmcopex  30115  nmcoplb  30116  lncnopbd  30123  nmcfnex  30139  nmcfnlb  30140  riesz4  30150  riesz1  30151  riesz2  30152  cnlnadjlem3  30155  cnlnadjlem5  30157  cnlnadjlem9  30161  cnlnadjeu  30164  rnbra  30193  pjimai  30262  pjclem4a  30284  pj3lem1  30292  jpi  30356  sumdmdii  30501  sumdmdlem  30504  sumdmdlem2  30505  cdjreui  30518  cdj3lem1  30520  iunin1f  30621  disjorf  30642  ofpreima  30727  1stpreima  30764  2ndpreima  30765  iocinioc2  30825  ssnnssfz  30833  cntzun  31044  isorng  31222  kerunit  31246  prmidl0  31345  ccfldextdgrr  31461  crefdf  31517  cmpcref  31519  cmppcmp  31527  cnre2csqima  31580  ordtconnlem1  31593  lmxrge0  31621  isrrext  31667  esum0  31734  esumcst  31748  esumpcvgval  31763  esumcvg  31771  measvuni  31899  eulerpartlemt0  32053  eulerpartlemr  32058  eulerpartlemgf  32063  eulerpartlemgs2  32064  eulerpartlemn  32065  fiblem  32082  oddprm2  32352  bnj521  32433  bnj1173  32700  bnj1174  32701  bnj1279  32716  elima4  33474  dfon2lem4  33486  frpoins3xpg  33529  frpoins3xp3g  33530  xpord3pred  33540  madeval2  33779  ellimits  33954  dfom5b  33956  brapply  33982  brcap  33984  dfrecs2  33994  dfrdg4  33995  finminlem  34249  neibastop2lem  34291  neibastop2  34292  neifg  34302  tailfb  34308  onsucconni  34368  onintopssconn  34371  onsucsuccmpi  34374  limsucncmpi  34376  onint1  34380  bj-inrab  34857  bj-rcleqf  34957  bj-restuni  35008  bj-opelresdm  35056  bj-idres  35071  bj-opelidres  35072  bj-eldiag  35087  bj-eldiag2  35088  bj-ccinftydisj  35124  taupilem3  35229  isbasisrelowllem1  35268  isbasisrelowllem2  35269  nlpineqsn  35321  fvineqsneu  35324  ptrest  35518  poimirlem29  35548  poimirlem30  35549  mblfinlem2  35557  mbfposadd  35566  itg2gt0cn  35574  dvasin  35603  inixp  35628  0totbnd  35673  sstotbnd3  35676  heibor1lem  35709  heibor1  35710  heiborlem6  35716  isexid2  35755  smgrpismgmOLD  35762  issmgrpOLD  35763  mndoissmgrpOLD  35768  ismndo  35772  exidresid  35779  rngo1cl  35839  isfld2  35905  ineleq  36228  eleccossin  36343  elrefsymrelsrel  36427  dfeldisj3  36572  prtlem14  36630  lshpdisj  36743  lkrin  36920  ishlat1  37108  pmodlem2  37603  pclfinN  37656  pclcmpatN  37657  osumcllem4N  37715  pexmidlem1N  37726  dihmeetlem1N  39046  dihglblem5apreN  39047  dihmeetlem4preN  39062  dihmeetlem13N  39075  dochnel2  39148  lcdlss  39375  mapd1o  39404  baerlem3lem2  39466  baerlem5alem2  39467  baerlem5blem2  39468  mhphf  40003  cmpfiiin  40230  mrefg2  40240  fz1eqin  40302  fnwe2lem2  40587  islmodfg  40605  islssfg2  40607  lnr2i  40652  rp-fakeinunass  40815  fiinfi  40864  elinintab  40867  elinintrab  40869  elinlem  40890  cnvcnvintabd  40892  ntrneikb  41389  ntrneik3  41391  ntrneik13  41393  ismnushort  41600  radcnvrat  41613  nzin  41617  onfrALTlem2  41847  onfrALTlem2VD  42190  inn0f  42302  iooabslt  42720  iccintsng  42744  lptioo2cn  42869  lptioo1cn  42870  cncfuni  43110  icccncfext  43111  stoweidlem44  43268  fourierdlem42  43373  fourierdlem80  43410  sge00  43597  eldmressn  44211  afvres  44344  afv2res  44411  prproropf1olem0  44635  31prm  44730  rnghmval2  45134  rnghmsubcsetclem1  45214  rngccatidALTV  45228  funcrngcsetcALT  45238  zrinitorngc  45239  zrtermorngc  45240  rhmsubcsetclem1  45260  rhmsubcrngclem1  45266  ringcbasbas  45273  funcringcsetcALTV2lem7  45281  ringccatidALTV  45291  ringcbasbasALTV  45297  funcringcsetclem7ALTV  45304  irinitoringc  45308  zrtermoringc  45309  srhmsubclem1  45312  fldhmsubc  45323  fldhmsubcALTV  45341  rhmsubcALTVlem3  45345  ssnn0ssfz  45366  elbigo2  45579  itsclinecirc0in  45802  opndisj  45877  clddisj  45878  i0oii  45894  io1ii  45895
  Copyright terms: Public domain W3C validator