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

Theorem elin 3662
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 3089 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3089 . . 3 (𝐴𝐶𝐴 ∈ V)
32adantl 480 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2580 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2580 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
64, 5anbi12d 742 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
7 df-in 3451 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
86, 7elab2g 3226 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
91, 3, 8pm5.21nii 366 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382   = wceq 1474  wcel 1938  Vcvv 3077  cin 3443
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-v 3079  df-in 3451
This theorem is referenced by:  elind  3663  elinel1  3664  elinel2  3665  elin2  3666  elin1d  3667  elin2d  3668  elin3  3669  incom  3670  ineqri  3671  ineq1  3672  inass  3688  inss1  3698  ssin  3700  ssrin  3703  dfss4  3723  difin  3726  indi  3735  undi  3736  unineq  3739  indifdir  3745  difin2  3752  inrab2  3762  difin0ss  3803  inssdif0  3804  inelcm  3887  inundif  3901  uniin  4291  intun  4342  intpr  4343  elrint  4351  iunin2  4418  iinin2  4424  elriin  4427  disjor  4465  disjiun  4471  brin  4532  trin  4589  inex1  4626  inuni  4652  wefrc  4926  inopab  5066  inxp  5068  dmin  5145  opelres  5213  eldmeldmressn  5251  intasym  5321  asymref  5322  dminss  5356  imainss  5357  inimasn  5359  ssrnres  5381  cnvresima  5431  dfco2a  5442  predel  5504  ordtri3or  5562  2elresin  5801  respreima  6135  fvcofneq  6158  tpres  6247  isomin  6363  isoini  6364  offval  6676  ordpwsuc  6781  ressuppss  7074  wfrlem5  7179  erdisj  7555  uniinqs  7588  mapval2  7647  ixpin  7693  boxriin  7710  disjen  7876  ssenen  7893  onfin2  7911  elfpw  8025  fiin  8085  inf3lem2  8283  epfrs  8364  cp  8511  bnd2  8513  dfac5lem1  8703  dfac5lem5  8707  dfac5  8708  kmlem3  8731  kmlem14  8742  kmlem15  8743  fin23lem26  8904  isfin1-3  8965  pwxpndom2  9240  ingru  9390  gruina  9393  grur1  9395  axgroth4  9407  grothprim  9409  ixxdisj  11926  icodisj  12033  fzdisj  12103  uzdisj  12146  nn0disj  12188  fzouzdisj  12237  xpcogend  13415  cotr2g  13417  limsupgle  13914  ello12  13956  elo12  13967  lo1resb  14004  rlimresb  14005  o1resb  14006  lo1eq  14008  rlimeq  14009  fsumsplit  14182  sumsplit  14205  fsum2dlem  14207  explecnv  14300  fprod2dlem  14413  bitsmod  14864  saddisjlem  14892  sadadd  14895  sadass  14899  smuval2  14910  smupval  14916  smueqlem  14918  smumul  14921  isprm7  15138  prmreclem5  15350  prmrec  15352  4sqlem12  15386  vdwmc  15408  acsfn  16039  iszeroo  16371  iszeroi  16378  isdrs2  16658  fpwipodrs  16883  psss  16933  subgacs  17348  nsgacs  17349  resscntz  17483  gsmsymgreq  17571  sylow2a  17769  lsmmod  17823  lsmdisj2  17830  gsumzsplit  18061  subgdmdprd  18167  dprdcntz2  18171  dprddisj2  18172  pgpfac1lem3  18210  isrhm  18455  subsubrg2  18541  lssacs  18696  lspdisj  18854  lspdisjb  18855  isassa  19044  aspid  19059  aspval2  19076  dfprm2  19571  ocvin  19744  unocv  19750  iunocv  19751  obselocv  19798  pmatcoe1fsupp  20232  isbasis2g  20470  tgval2  20478  tgcl  20491  ppttop  20528  epttop  20530  clsval2  20571  ssntr  20579  ntreq0  20598  isclo  20608  restntr  20703  restlp  20704  cnpresti  20809  cnprest  20810  cnprest2  20811  lmss  20819  haust1  20873  nrmsep3  20876  isnrm2  20879  lmmo  20901  fincmp  20913  0cmp  20914  discmp  20918  cmpsublem  20919  cmpsub  20920  uncmp  20923  hauscmplem  20926  dfcon2  20939  iunconlem  20947  uncon  20949  is1stc2  20962  1stcrest  20973  1stcelcls  20981  llyi  20994  nllyi  20995  subislly  21001  lly1stc  21016  comppfsc  21052  txcnp  21140  txcnmpt  21144  hausdiag  21165  kqcldsat  21253  ptcmpfi  21333  isfbas2  21356  isfil2  21377  fbasfip  21389  elfg  21392  filcon  21404  rnelfmlem  21473  rnelfm  21474  fmfnfmlem2  21476  fmfnfmlem4  21478  fmfnfm  21479  flimrest  21504  hauspwpwf1  21508  fclsrest  21545  alexsubALTlem2  21569  alexsubALTlem3  21570  alexsubALTlem4  21571  alexsubALT  21572  ptcmp  21579  istmd  21595  istgp  21598  tsmssubm  21663  tsmssplit  21672  istrg  21684  istdrg  21686  istlm  21705  ustfilxp  21733  utoptop  21755  utop3cls  21772  bldisj  21919  blin  21942  blin2  21950  blres  21952  lpbl  22024  metrest  22045  restmetu  22091  isngp  22116  isnlm  22184  isnmhm  22273  xrtgioo  22330  xrsmopn  22336  icccmplem2  22347  reconnlem2  22351  icoopnst  22473  iocopnst  22474  bndth  22492  iscph  22655  tchcph  22718  cfilfcls  22751  cmetcaulem  22765  cmetss  22791  isbn  22813  cldcss2  22903  hlhil  22904  ovolfcl  22926  ovolicc1  22976  ovolicc2lem2  22978  ovolicc2lem4OLD  22980  ovolicc2lem4  22981  ovolicc2lem5  22982  ovolicc2  22983  shftmbl  22999  volfiniun  23008  ioorf  23033  mbfmax  23108  mbfimaopnlem  23114  mbfaddlem  23119  mbfadd  23120  mbfsub  23121  i1faddlem  23152  i1fmullem  23153  i1fres  23164  itg1climres  23173  mbfi1fseqlem4  23177  mbfmul  23185  itg2splitlem  23207  itg2split  23208  itgresr  23237  bddmulibl  23297  ellimc2  23333  ellimc3  23335  limcun  23351  dvreslem  23365  dvne0  23464  itgsubstlem  23501  ig1pval3  23627  ig1pval3OLD  23633  aaliou2  23797  aaliou2b  23798  pilem1  23907  rlimcnp2  24391  fsumharmonic  24436  ppisval2  24531  prmorcht  24604  fsumvma2  24639  pclogsum  24640  vmasum  24641  chpchtsum  24644  chpub  24645  chebbnd1lem1  24858  rpvmasum2  24901  tglineineq  25239  frgrancvvdeqlem4  26309  frgrancvvdeqlem7  26312  frgrancvvdeqlemA  26313  frgrancvvdeqlemC  26315  minvecolem1  26903  minvecolem4a  26906  minvecolem4b  26907  minvecolem4  26909  minvecolem4aOLD  26916  minvecolem4bOLD  26917  minvecolem4OLD  26919  h2hcau  27019  axhcompl-zf  27038  hhcmpl  27240  hhcms  27243  ocin  27338  ocnel  27340  shmodsi  27431  pjhthlem2  27434  omlsilem  27444  pjoc1i  27473  spansnm0i  27692  nonbooli  27693  5oalem7  27702  3oalem3  27706  pjssmii  27723  mayete3i  27770  nmcopex  28071  nmcoplb  28072  lncnopbd  28079  nmcfnex  28095  nmcfnlb  28096  riesz4  28106  riesz1  28107  riesz2  28108  cnlnadjlem3  28111  cnlnadjlem5  28113  cnlnadjlem9  28117  cnlnadjeu  28120  rnbra  28149  pjimai  28218  pjclem4a  28240  pj3lem1  28248  jpi  28312  sumdmdii  28457  sumdmdlem  28460  sumdmdlem2  28461  cdjreui  28474  cdj3lem1  28476  iunin1f  28556  disjorf  28573  ofpreima  28647  1stpreima  28666  2ndpreima  28667  iocinioc2  28737  ssnnssfz  28743  isorng  28937  kerunit  28961  crefdf  29050  cmpcref  29052  cmppcmp  29060  pcmplfin  29062  cnre2csqima  29092  ordtconlem1  29105  lmxrge0  29133  isrrext  29179  esum0  29245  esumcst  29259  esumpcvgval  29274  esumcvg  29282  measvuni  29411  eulerpartlemt0  29576  eulerpartlemr  29581  eulerpartlemgf  29586  eulerpartlemgs2  29587  eulerpartlemn  29588  sseqf  29599  fiblem  29605  bnj521  29915  bnj1172  30179  bnj1173  30180  bnj1174  30181  bnj1279  30196  dfres3  30755  elima4  30777  dfon2lem4  30788  frrlem5  30874  ellimits  31033  dfom5b  31035  brapply  31061  brcap  31063  dfrecs2  31073  dfrdg4  31074  finminlem  31328  neibastop2lem  31370  neibastop2  31371  neifg  31381  tailfb  31387  onsucconi  31451  onintopsscon  31454  onsucsuccmpi  31457  limsucncmpi  31459  onint1  31463  bj-inrab  31957  bj-restuni  32073  bj-eldiag  32110  bj-eldiag2  32111  bj-ccinftydisj  32119  taupilem3  32184  isbasisrelowllem1  32222  isbasisrelowllem2  32223  ptrest  32444  poimirlem29  32474  poimirlem30  32475  mblfinlem2  32483  mbfposadd  32493  itg2gt0cn  32501  dvasin  32532  inixp  32559  0totbnd  32608  sstotbnd3  32611  heibor1lem  32644  heibor1  32645  heiborlem6  32651  isexid2  32690  smgrpismgmOLD  32697  issmgrpOLD  32698  mndoissmgrpOLD  32703  mndoisexid  32704  ismndo  32707  exidresid  32714  rngo1cl  32774  isfld2  32840  prtlem14  33043  lshpdisj  33158  lkrin  33335  ishlat1  33523  pmodlem2  34017  pclfinN  34070  pclcmpatN  34071  osumcllem4N  34129  pexmidlem1N  34140  dihmeetlem1N  35463  dihglblem5apreN  35464  dihmeetlem4preN  35479  dihmeetlem13N  35492  dochnel2  35565  lcdlss  35792  mapd1o  35821  baerlem3lem2  35883  baerlem5alem2  35884  baerlem5blem2  35885  cmpfiiin  36144  mrefg2  36154  fz1eqin  36216  fnwe2lem2  36509  islmodfg  36527  islssfg2  36529  lnr2i  36575  acsfn1p  36665  subrgacs  36666  sdrgacs  36667  rp-fakeinunass  36757  fiinfi  36774  elinintab  36777  elinintrab  36779  elinlem  36800  cnvcnvintabd  36802  ndisj  36960  ntrneikb  37289  ntrneik3  37291  ntrneik13  37293  radcnvrat  37412  nzin  37416  onfrALTlem2  37659  onfrALTlem2VD  38024  elini  38113  inn0f  38146  iooabslt  38450  iccintsng  38478  lptioo2cn  38598  lptioo1cn  38599  cncfuni  38658  icccncfext  38659  stoweidlem44  38826  fourierdlem42  38932  fourierdlem42OLD  38933  fourierdlem80  38970  sge00  39162  eldmressn  39745  afvres  39795  31prm  39944  trlsegvdeg  41486  frgrncvvdeqlem4  41563  frgrncvvdeqlem7  41566  frgrncvvdeqlemA  41567  frgrncvvdeqlemC  41569  rnghmval2  41776  rnghmsubcsetclem1  41858  rngccatidALTV  41872  funcrngcsetcALT  41882  zrinitorngc  41883  zrtermorngc  41884  rhmsubcsetclem1  41904  rhmsubcrngclem1  41910  ringcbasbas  41917  funcringcsetcALTV2lem7  41925  ringccatidALTV  41935  ringcbasbasALTV  41941  funcringcsetclem7ALTV  41948  irinitoringc  41952  zrtermoringc  41953  srhmsubclem1  41956  fldhmsubc  41967  srhmsubcALTVlem1  41975  fldhmsubcALTV  41986  rhmsubcALTVlem3  41990  ssnn0ssfz  42011  elbigo2  42235
  Copyright terms: Public domain W3C validator