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

Theorem elin 4167
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 3511 . 2 (𝐴 ∈ (𝐵𝐶) → 𝐴 ∈ V)
2 elex 3511 . . 3 (𝐴𝐶𝐴 ∈ V)
32adantl 484 . 2 ((𝐴𝐵𝐴𝐶) → 𝐴 ∈ V)
4 eleq1 2898 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 eleq1 2898 . . . 4 (𝑥 = 𝐴 → (𝑥𝐶𝐴𝐶))
64, 5anbi12d 632 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝐶) ↔ (𝐴𝐵𝐴𝐶)))
7 df-in 3941 . . 3 (𝐵𝐶) = {𝑥 ∣ (𝑥𝐵𝑥𝐶)}
86, 7elab2g 3666 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶)))
91, 3, 8pm5.21nii 382 1 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wa 398   = wceq 1531  wcel 2108  Vcvv 3493  cin 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-in 3941
This theorem is referenced by:  elini  4168  elind  4169  elinel1  4170  elinel2  4171  elin2  4172  elin3  4175  incomOLD  4177  ineqri  4178  ineq1OLD  4180  inass  4194  ssin  4205  ssrin  4208  rexin  4214  dfss4  4233  difin  4236  indi  4248  undi  4249  unineq  4252  indifdir  4258  difin2  4264  inrab2  4274  ndisj  4325  difin0ss  4326  inssdif0  4327  inelcm  4412  inundif  4425  elinsn  4638  uniin  4850  intun  4899  intpr  4900  elrint  4908  iunin2  4984  iinin2  4991  elriin  4994  disjor  5037  disjiun  5044  brin  5109  trin  5173  inex1  5212  inuni  5237  wefrc  5542  inopab  5694  inxp  5696  dmin  5773  dfres3  5851  intasym  5968  asymref  5969  dminss  6003  imainss  6004  inimasn  6006  cnvresima  6080  dfco2a  6092  ordtri3or  6216  2elresin  6461  respreima  6829  fvcofneq  6852  tpres  6956  isomin  7082  isoini  7083  offval  7408  ordpwsuc  7522  ressuppss  7841  wfrlem5  7951  uniinqs  8369  mapval2  8428  ixpin  8479  boxriin  8496  disjen  8666  ssenen  8683  onfin2  8702  elfpw  8818  fiin  8878  inf3lem2  9084  epfrs  9165  cp  9312  dfac5lem1  9541  dfac5lem5  9545  dfac5  9546  kmlem3  9570  kmlem14  9581  kmlem15  9582  fin23lem26  9739  pwxpndom2  10079  ingru  10229  gruina  10232  grur1  10234  axgroth4  10246  grothprim  10248  ixxdisj  12745  icodisj  12854  fzdisj  12926  nn0disj  13015  fzouzdisj  13065  cotr2g  14328  limsupgle  14826  ello12  14865  elo12  14876  lo1resb  14913  rlimresb  14914  o1resb  14915  lo1eq  14917  rlimeq  14918  fsumsplit  15089  sumsplit  15115  fsum2dlem  15117  fprod2dlem  15326  bitsmod  15777  saddisjlem  15805  sadadd  15808  sadass  15812  smuval2  15823  smupval  15829  smueqlem  15831  smumul  15834  isprm7  16044  prmreclem5  16248  prmrec  16250  4sqlem12  16284  vdwmc  16306  setsstruct2  16513  acsfn  16922  iszeroo  17254  iszeroi  17261  fpwipodrs  17766  psss  17816  insubm  17975  subgacs  18305  nsgacs  18306  resscntz  18454  gsmsymgreq  18552  sylow2a  18736  lsmmod  18793  lsmdisj2  18800  gsumzsplit  19039  subgdmdprd  19148  dprdcntz2  19152  dprddisj2  19153  pgpfac1lem3  19191  isrhm  19465  subsubrg2  19554  acsfn1p  19570  subrgacs  19571  sdrgacs  19572  lssacs  19731  lspdisj  19889  lspdisjb  19890  isassa  20080  aspid  20096  aspval2  20119  dfprm2  20633  ocvin  20810  unocv  20816  iunocv  20817  obselocv  20864  pmatcoe1fsupp  21301  isbasis2g  21548  tgval2  21556  tgcl  21569  ppttop  21607  epttop  21609  ssntr  21658  ntreq0  21677  isclo  21687  restntr  21782  restlp  21783  cnpresti  21888  cnprest  21889  cnprest2  21890  lmss  21898  haust1  21952  nrmsep3  21955  isnrm2  21958  lmmo  21980  fincmp  21993  cmpsublem  21999  cmpsub  22000  uncmp  22003  hauscmplem  22006  dfconn2  22019  iunconnlem  22027  unconn  22029  is1stc2  22042  1stcrest  22053  1stcelcls  22061  llyi  22074  nllyi  22075  subislly  22081  lly1stc  22096  txcnp  22220  txcnmpt  22224  hausdiag  22245  kqcldsat  22333  isfbas2  22435  isfil2  22456  fbasfip  22468  elfg  22471  filconn  22483  rnelfmlem  22552  rnelfm  22553  fmfnfmlem2  22555  fmfnfmlem4  22557  fmfnfm  22558  flimrest  22583  hauspwpwf1  22587  fclsrest  22624  alexsubALTlem2  22648  alexsubALTlem3  22649  alexsubALTlem4  22650  alexsubALT  22651  istmd  22674  istgp  22677  tsmssubm  22743  tsmssplit  22752  istrg  22764  istdrg  22766  istlm  22785  ustfilxp  22813  utoptop  22835  utop3cls  22852  bldisj  23000  blin  23023  blres  23033  lpbl  23105  metrest  23126  restmetu  23172  isngp  23197  isnlm  23276  isnmhm  23347  xrtgioo  23406  xrsmopn  23412  icccmplem2  23423  reconnlem2  23427  icoopnst  23535  iocopnst  23536  bndth  23554  zclmncvs  23744  isncvsngp  23745  ncvsprp  23748  ncvsm1  23750  ncvsdif  23751  ncvspi  23752  ncvs1  23753  ncvspds  23757  iscph  23766  tcphcph  23832  cfilfcls  23869  cmetcaulem  23883  isbn  23933  cldcss2  24037  hlhil  24038  ovolfcl  24059  ovolicc2lem2  24111  ovolicc2  24115  shftmbl  24131  volfiniun  24140  mbfmax  24242  mbfimaopnlem  24248  mbfaddlem  24253  i1faddlem  24286  i1fmullem  24287  i1fres  24298  itg1climres  24307  mbfi1fseqlem4  24311  itg2splitlem  24341  itg2split  24342  itgresr  24371  ellimc2  24467  ellimc3  24469  limcun  24485  dvreslem  24499  dvne0  24600  itgsubstlem  24637  ig1pval3  24760  aaliou2  24921  aaliou2b  24922  pilem1  25031  rlimcnp2  25536  fsumharmonic  25581  ppisval2  25674  prmorcht  25747  fsumvma2  25782  pclogsum  25783  vmasum  25784  chpchtsum  25787  chpub  25788  rpvmasum2  26080  tglineineq  26421  trlsegvdeg  27998  frgrncvvdeqlem7  28076  frgrncvvdeqlem9  28078  minvecolem1  28643  minvecolem4a  28646  minvecolem4b  28647  minvecolem4  28649  h2hcau  28748  axhcompl-zf  28767  hhcmpl  28969  hhcms  28972  ocin  29065  ocnel  29067  shmodsi  29158  pjhthlem2  29161  omlsilem  29171  pjoc1i  29200  spansnm0i  29419  nonbooli  29420  5oalem7  29429  3oalem3  29433  pjssmii  29450  mayete3i  29497  nmcopex  29798  nmcoplb  29799  lncnopbd  29806  nmcfnex  29822  nmcfnlb  29823  riesz4  29833  riesz1  29834  riesz2  29835  cnlnadjlem3  29838  cnlnadjlem5  29840  cnlnadjlem9  29844  cnlnadjeu  29847  rnbra  29876  pjimai  29945  pjclem4a  29967  pj3lem1  29975  jpi  30039  sumdmdii  30184  sumdmdlem  30187  sumdmdlem2  30188  cdjreui  30201  cdj3lem1  30203  iunin1f  30301  disjorf  30321  ofpreima  30402  1stpreima  30434  2ndpreima  30435  iocinioc2  30494  ssnnssfz  30502  cntzun  30688  isorng  30865  kerunit  30889  ccfldextdgrr  31050  crefdf  31105  cmpcref  31107  cmppcmp  31115  cnre2csqima  31147  ordtconnlem1  31160  lmxrge0  31188  isrrext  31234  esum0  31301  esumcst  31315  esumpcvgval  31330  esumcvg  31338  measvuni  31466  eulerpartlemt0  31620  eulerpartlemr  31625  eulerpartlemgf  31630  eulerpartlemgs2  31631  eulerpartlemn  31632  fiblem  31649  oddprm2  31919  bnj521  32000  bnj1173  32267  bnj1174  32268  bnj1279  32283  elima4  33012  dfon2lem4  33024  frrlem13  33128  fprlem1  33130  madeval2  33283  ellimits  33364  dfom5b  33366  brapply  33392  brcap  33394  dfrecs2  33404  dfrdg4  33405  finminlem  33659  neibastop2lem  33701  neibastop2  33702  neifg  33712  tailfb  33718  onsucconni  33778  onintopssconn  33781  onsucsuccmpi  33784  limsucncmpi  33786  onint1  33790  bj-inrab  34238  bj-rcleqf  34330  bj-restuni  34380  bj-opelresdm  34429  bj-idres  34444  bj-opelidres  34445  bj-eldiag  34460  bj-eldiag2  34461  bj-ccinftydisj  34487  taupilem3  34592  isbasisrelowllem1  34628  isbasisrelowllem2  34629  nlpineqsn  34681  fvineqsneu  34684  ptrest  34883  poimirlem29  34913  poimirlem30  34914  mblfinlem2  34922  mbfposadd  34931  itg2gt0cn  34939  dvasin  34970  inixp  34995  0totbnd  35043  sstotbnd3  35046  heibor1lem  35079  heibor1  35080  heiborlem6  35086  isexid2  35125  smgrpismgmOLD  35132  issmgrpOLD  35133  mndoissmgrpOLD  35138  ismndo  35142  exidresid  35149  rngo1cl  35209  isfld2  35275  ineleq  35600  eleccossin  35715  elrefsymrelsrel  35799  dfeldisj3  35944  prtlem14  36002  lshpdisj  36115  lkrin  36292  ishlat1  36480  pmodlem2  36975  pclfinN  37028  pclcmpatN  37029  osumcllem4N  37087  pexmidlem1N  37098  dihmeetlem1N  38418  dihglblem5apreN  38419  dihmeetlem4preN  38434  dihmeetlem13N  38447  dochnel2  38520  lcdlss  38747  mapd1o  38776  baerlem3lem2  38838  baerlem5alem2  38839  baerlem5blem2  38840  cmpfiiin  39284  mrefg2  39294  fz1eqin  39356  fnwe2lem2  39641  islmodfg  39659  islssfg2  39661  lnr2i  39706  rp-fakeinunass  39871  fiinfi  39922  elinintab  39925  elinintrab  39927  elinlem  39948  cnvcnvintabd  39950  ntrneikb  40434  ntrneik3  40436  ntrneik13  40438  radcnvrat  40636  nzin  40640  onfrALTlem2  40870  onfrALTlem2VD  41213  inn0f  41325  iooabslt  41763  iccintsng  41788  lptioo2cn  41915  lptioo1cn  41916  cncfuni  42158  icccncfext  42159  stoweidlem44  42319  fourierdlem42  42424  fourierdlem80  42461  sge00  42648  eldmressn  43262  afvres  43361  afv2res  43428  prproropf1olem0  43654  31prm  43750  rnghmval2  44156  rnghmsubcsetclem1  44236  rngccatidALTV  44250  funcrngcsetcALT  44260  zrinitorngc  44261  zrtermorngc  44262  rhmsubcsetclem1  44282  rhmsubcrngclem1  44288  ringcbasbas  44295  funcringcsetcALTV2lem7  44303  ringccatidALTV  44313  ringcbasbasALTV  44319  funcringcsetclem7ALTV  44326  irinitoringc  44330  zrtermoringc  44331  srhmsubclem1  44334  fldhmsubc  44345  fldhmsubcALTV  44363  rhmsubcALTVlem3  44367  ssnn0ssfz  44387  elbigo2  44602  itsclinecirc0in  44752
  Copyright terms: Public domain W3C validator