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

Theorem elin 3829
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 3243 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3243 . . 3 (𝐴𝐶𝐴 ∈ V)
32adantl 481 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2718 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2718 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
64, 5anbi12d 747 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
7 df-in 3614 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
86, 7elab2g 3385 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
91, 3, 8pm5.21nii 367 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1523  wcel 2030  Vcvv 3231  cin 3606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614
This theorem is referenced by:  elini  3830  elind  3831  elinel1  3832  elinel2  3833  elin2  3834  elin3  3837  incom  3838  ineqri  3839  ineq1  3840  inass  3856  ssin  3868  ssrin  3871  dfss4  3891  difin  3894  indi  3906  undi  3907  unineq  3910  indifdir  3916  difin2  3923  inrab2  3933  difin0ss  3979  inssdif0  3980  inelcm  4065  inundif  4079  elinsn  4277  uniin  4489  intun  4541  intpr  4542  elrint  4550  iunin2  4616  iinin2  4622  elriin  4625  disjor  4666  disjiun  4672  brin  4737  trin  4796  inex1  4832  inuni  4856  wefrc  5137  inopab  5285  inxp  5287  dmin  5364  dfres3  5433  opelresg  5434  opelresOLD  5438  intasym  5546  asymref  5547  dminss  5582  imainss  5583  inimasn  5585  ssrnres  5607  cnvresima  5661  dfco2a  5673  ordtri3or  5793  2elresin  6040  respreima  6384  fvcofneq  6407  tpres  6507  isomin  6627  isoini  6628  offval  6946  ordpwsuc  7057  ressuppss  7359  wfrlem5  7464  erdisj  7837  uniinqs  7870  mapval2  7929  ixpin  7975  boxriin  7992  disjen  8158  ssenen  8175  onfin2  8193  elfpw  8309  fiin  8369  inf3lem2  8564  epfrs  8645  cp  8792  bnd2  8794  dfac5lem1  8984  dfac5lem5  8988  dfac5  8989  kmlem3  9012  kmlem14  9023  kmlem15  9024  fin23lem26  9185  isfin1-3  9246  pwxpndom2  9525  ingru  9675  gruina  9678  grur1  9680  axgroth4  9692  grothprim  9694  ixxdisj  12228  icodisj  12335  fzdisj  12406  uzdisj  12451  nn0disj  12494  fzouzdisj  12543  xpcogend  13759  cotr2g  13761  limsupgle  14252  ello12  14291  elo12  14302  lo1resb  14339  rlimresb  14340  o1resb  14341  lo1eq  14343  rlimeq  14344  fsumsplit  14515  sumsplit  14543  fsum2dlem  14545  explecnv  14641  fprod2dlem  14754  bitsmod  15205  saddisjlem  15233  sadadd  15236  sadass  15240  smuval2  15251  smupval  15257  smueqlem  15259  smumul  15262  isprm7  15467  prmreclem5  15671  prmrec  15673  4sqlem12  15707  vdwmc  15729  setsstruct2  15943  acsfn  16367  iszeroo  16699  iszeroi  16706  isdrs2  16986  fpwipodrs  17211  psss  17261  subgacs  17676  nsgacs  17677  resscntz  17810  gsmsymgreq  17898  sylow2a  18080  lsmmod  18134  lsmdisj2  18141  gsumzsplit  18373  subgdmdprd  18479  dprdcntz2  18483  dprddisj2  18484  pgpfac1lem3  18522  isrhm  18769  subsubrg2  18855  lssacs  19015  lspdisj  19173  lspdisjb  19174  isassa  19363  aspid  19378  aspval2  19395  dfprm2  19890  ocvin  20066  unocv  20072  iunocv  20073  obselocv  20120  pmatcoe1fsupp  20554  isbasis2g  20800  tgval2  20808  tgcl  20821  ppttop  20859  epttop  20861  clsval2  20902  ssntr  20910  ntreq0  20929  isclo  20939  restntr  21034  restlp  21035  cnpresti  21140  cnprest  21141  cnprest2  21142  lmss  21150  haust1  21204  nrmsep3  21207  isnrm2  21210  lmmo  21232  fincmp  21244  0cmp  21245  discmp  21249  cmpsublem  21250  cmpsub  21251  uncmp  21254  hauscmplem  21257  dfconn2  21270  iunconnlem  21278  unconn  21280  is1stc2  21293  1stcrest  21304  1stcelcls  21312  llyi  21325  nllyi  21326  subislly  21332  lly1stc  21347  comppfsc  21383  txcnp  21471  txcnmpt  21475  hausdiag  21496  kqcldsat  21584  ptcmpfi  21664  isfbas2  21686  isfil2  21707  fbasfip  21719  elfg  21722  filconn  21734  rnelfmlem  21803  rnelfm  21804  fmfnfmlem2  21806  fmfnfmlem4  21808  fmfnfm  21809  flimrest  21834  hauspwpwf1  21838  fclsrest  21875  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALTlem4  21901  alexsubALT  21902  ptcmp  21909  istmd  21925  istgp  21928  tsmssubm  21993  tsmssplit  22002  istrg  22014  istdrg  22016  istlm  22035  ustfilxp  22063  utoptop  22085  utop3cls  22102  bldisj  22250  blin  22273  blin2  22281  blres  22283  lpbl  22355  metrest  22376  restmetu  22422  isngp  22447  isnlm  22526  isnmhm  22597  xrtgioo  22656  xrsmopn  22662  icccmplem2  22673  reconnlem2  22677  icoopnst  22785  iocopnst  22786  bndth  22804  cvsi  22976  cnstrcvs  22987  cncvs  22991  zclmncvs  22994  isncvsngp  22995  ncvsprp  22998  ncvsm1  23000  ncvsdif  23001  ncvspi  23002  ncvs1  23003  ncvspds  23007  iscph  23016  tchcph  23082  cfilfcls  23118  cmetcaulem  23132  cmetss  23159  isbn  23181  cldcss2  23259  hlhil  23260  ovolfcl  23281  ovolicc1  23330  ovolicc2lem2  23332  ovolicc2lem4  23334  ovolicc2lem5  23335  ovolicc2  23336  shftmbl  23352  volfiniun  23361  ioorf  23387  mbfmax  23461  mbfimaopnlem  23467  mbfaddlem  23472  mbfadd  23473  mbfsub  23474  i1faddlem  23505  i1fmullem  23506  i1fres  23517  itg1climres  23526  mbfi1fseqlem4  23530  mbfmul  23538  itg2splitlem  23560  itg2split  23561  itgresr  23590  bddmulibl  23650  ellimc2  23686  ellimc3  23688  limcun  23704  dvreslem  23718  dvne0  23819  itgsubstlem  23856  ig1pval3  23979  aaliou2  24140  aaliou2b  24141  pilem1  24250  rlimcnp2  24738  fsumharmonic  24783  ppisval2  24876  prmorcht  24949  fsumvma2  24984  pclogsum  24985  vmasum  24986  chpchtsum  24989  chpub  24990  chebbnd1lem1  25203  rpvmasum2  25246  tglineineq  25583  trlsegvdeg  27205  frgrncvvdeqlem7  27285  frgrncvvdeqlem9  27287  minvecolem1  27858  minvecolem4a  27861  minvecolem4b  27862  minvecolem4  27864  h2hcau  27964  axhcompl-zf  27983  hhcmpl  28185  hhcms  28188  ocin  28283  ocnel  28285  shmodsi  28376  pjhthlem2  28379  omlsilem  28389  pjoc1i  28418  spansnm0i  28637  nonbooli  28638  5oalem7  28647  3oalem3  28651  pjssmii  28668  mayete3i  28715  nmcopex  29016  nmcoplb  29017  lncnopbd  29024  nmcfnex  29040  nmcfnlb  29041  riesz4  29051  riesz1  29052  riesz2  29053  cnlnadjlem3  29056  cnlnadjlem5  29058  cnlnadjlem9  29062  cnlnadjeu  29065  rnbra  29094  pjimai  29163  pjclem4a  29185  pj3lem1  29193  jpi  29257  sumdmdii  29402  sumdmdlem  29405  sumdmdlem2  29406  cdjreui  29419  cdj3lem1  29421  iunin1f  29500  disjorf  29518  ofpreima  29593  1stpreima  29612  2ndpreima  29613  iocinioc2  29669  ssnnssfz  29677  isorng  29927  kerunit  29951  crefdf  30043  cmpcref  30045  cmppcmp  30053  pcmplfin  30055  cnre2csqima  30085  ordtconnlem1  30098  lmxrge0  30126  isrrext  30172  esum0  30239  esumcst  30253  esumpcvgval  30268  esumcvg  30276  measvuni  30405  eulerpartlemt0  30559  eulerpartlemr  30564  eulerpartlemgf  30569  eulerpartlemgs2  30570  eulerpartlemn  30571  fiblem  30588  oddprm2  30861  bnj521  30931  bnj1173  31196  bnj1174  31197  bnj1279  31212  elima4  31803  imaindm  31806  dfon2lem4  31815  frrlem5  31909  madeval2  32061  ellimits  32142  dfom5b  32144  brapply  32170  brcap  32172  dfrecs2  32182  dfrdg4  32183  finminlem  32437  neibastop2lem  32480  neibastop2  32481  neifg  32491  tailfb  32497  onsucconni  32561  onintopssconn  32564  onsucsuccmpi  32567  limsucncmpi  32569  onint1  32573  bj-inrab  33048  bj-restuni  33175  bj-eldiag  33221  bj-eldiag2  33222  bj-ccinftydisj  33230  taupilem3  33295  isbasisrelowllem1  33333  isbasisrelowllem2  33334  ptrest  33538  poimirlem29  33568  poimirlem30  33569  mblfinlem2  33577  mbfposadd  33587  itg2gt0cn  33595  dvasin  33626  inixp  33653  0totbnd  33702  sstotbnd3  33705  heibor1lem  33738  heibor1  33739  heiborlem6  33745  isexid2  33784  smgrpismgmOLD  33791  issmgrpOLD  33792  mndoissmgrpOLD  33797  ismndo  33801  exidresid  33808  rngo1cl  33868  isfld2  33934  ineleq  34259  eleccossin  34373  elrefsymrelsrel  34455  prtlem14  34478  lshpdisj  34592  lkrin  34769  ishlat1  34957  pmodlem2  35451  pclfinN  35504  pclcmpatN  35505  osumcllem4N  35563  pexmidlem1N  35574  dihmeetlem1N  36896  dihglblem5apreN  36897  dihmeetlem4preN  36912  dihmeetlem13N  36925  dochnel2  36998  lcdlss  37225  mapd1o  37254  baerlem3lem2  37316  baerlem5alem2  37317  baerlem5blem2  37318  cmpfiiin  37577  mrefg2  37587  fz1eqin  37649  fnwe2lem2  37938  islmodfg  37956  islssfg2  37958  lnr2i  38003  acsfn1p  38086  subrgacs  38087  sdrgacs  38088  rp-fakeinunass  38178  fiinfi  38195  elinintab  38198  elinintrab  38200  elinlem  38221  cnvcnvintabd  38223  ndisj  38380  ntrneikb  38709  ntrneik3  38711  ntrneik13  38713  radcnvrat  38830  nzin  38834  onfrALTlem2  39078  onfrALTlem2VD  39439  inn0f  39556  iooabslt  40039  iccintsng  40067  lptioo2cn  40195  lptioo1cn  40196  cncfuni  40417  icccncfext  40418  stoweidlem44  40579  fourierdlem42  40684  fourierdlem80  40721  sge00  40911  eldmressn  41524  afvres  41573  31prm  41837  rnghmval2  42220  rnghmsubcsetclem1  42300  rngccatidALTV  42314  funcrngcsetcALT  42324  zrinitorngc  42325  zrtermorngc  42326  rhmsubcsetclem1  42346  rhmsubcrngclem1  42352  ringcbasbas  42359  funcringcsetcALTV2lem7  42367  ringccatidALTV  42377  ringcbasbasALTV  42383  funcringcsetclem7ALTV  42390  irinitoringc  42394  zrtermoringc  42395  srhmsubclem1  42398  fldhmsubc  42409  fldhmsubcALTV  42427  rhmsubcALTVlem3  42431  ssnn0ssfz  42452  elbigo2  42671
  Copyright terms: Public domain W3C validator