Theorem elin 3960

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.

Step	Hyp	Ref	Expression
1		elex 3480	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3480	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 480	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2813	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2813	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 630	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3951	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3666	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 377	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  Vcvv 3461   ∩ cin 3943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-in 3951

This theorem is referenced by:  elini  4191  elind  4192  elinel1  4193  elinel2  4194  elin2  4195  elin3  4198  ineqri  4202  nfin  4214  inass  4218  ssin  4229  ssrin  4232  rexin  4238  dfss4  4257  difin  4260  indi  4272  undi  4273  unineq  4276  indifdi  4282  indifdirOLD  4284  difin2  4290  inrab2  4306  ndisj  4367  inn0f  4368  difin0ss  4370  inssdif0  4371  inelcm  4466  inundif  4480  elinsn  4716  uniin  4935  intun  4984  intprg  4985  intprOLD  4987  elrint  4995  iunin2  5075  iinin2  5082  elriin  5085  disjor  5129  disjiun  5136  brin  5201  trin  5278  inex1  5318  inuni  5346  wefrc  5672  inopab  5831  inxp  5834  inxpOLD  5835  dmin  5914  dfres3  5990  intasym  6122  asymref  6123  dminss  6159  imainss  6160  inimasn  6162  cnvresima  6236  dfco2a  6252  ordtri3or  6403  2elresin  6677  respreima  7074  fvcofneq  7102  tpres  7213  isomin  7344  isoini  7345  offval  7694  ordpwsuc  7819  frpoins3xpg  8145  frpoins3xp3g  8146  xpord3pred  8157  ressuppss  8188  frrlem13  8304  fprlem1  8306  wfrlem5OLD  8334  uniinqs  8816  mapval2  8891  ixpin  8942  boxriin  8959  disjen  9159  ssenen  9176  onfin2  9256  elfpw  9380  fiin  9447  inf3lem2  9654  epfrs  9756  cp  9916  dfac5lem1  10148  dfac5lem5  10152  dfac5  10153  kmlem3  10177  kmlem14  10188  kmlem15  10189  fin23lem26  10350  pwxpndom2  10690  ingru  10840  gruina  10843  grur1  10845  axgroth4  10857  grothprim  10859  ixxdisj  13374  icodisj  13488  fzdisj  13563  nn0disj  13652  fzouzdisj  13703  cotr2g  14959  limsupgle  15457  ello12  15496  elo12  15507  lo1resb  15544  rlimresb  15545  o1resb  15546  lo1eq  15548  rlimeq  15549  fsumsplit  15723  sumsplit  15750  fsum2dlem  15752  fprod2dlem  15960  bitsmod  16414  saddisjlem  16442  sadadd  16445  sadass  16449  smuval2  16460  smupval  16466  smueqlem  16468  smumul  16471  isprm7  16682  prmreclem5  16892  prmrec  16894  4sqlem12  16928  vdwmc  16950  setsstruct2  17146  acsfn  17642  iszeroo  17990  iszeroi  18001  fpwipodrs  18535  psss  18575  insubm  18778  subgacs  19124  nsgacs  19125  resscntz  19296  gsmsymgreq  19399  sylow2a  19586  lsmmod  19642  lsmdisj2  19649  gsumzsplit  19894  subgdmdprd  20003  dprdcntz2  20007  dprddisj2  20008  pgpfac1lem3  20046  rnghmval2  20395  isrhm  20429  subsubrng2  20513  subsubrg2  20550  rnghmsubcsetclem1  20576  funcrngcsetcALT  20586  zrinitorngc  20587  zrtermorngc  20588  rhmsubcsetclem1  20605  rhmsubcrngclem1  20611  ringcbasbas  20618  zrtermoringc  20620  srhmsubclem1  20622  fldhmsubc  20685  acsfn1p  20699  subrgacs  20700  sdrgacs  20701  lssacs  20863  lspdisj  21025  lspdisjb  21026  dfprm2  21416  irinitoringc  21422  ocvin  21623  unocv  21629  iunocv  21630  obselocv  21679  isassa  21807  aspid  21825  aspval2  21848  pmatcoe1fsupp  22647  isbasis2g  22895  tgval2  22903  tgcl  22916  ppttop  22954  epttop  22956  ssntr  23006  ntreq0  23025  isclo  23035  restntr  23130  restlp  23131  cnpresti  23236  cnprest  23237  cnprest2  23238  lmss  23246  haust1  23300  nrmsep3  23303  isnrm2  23306  lmmo  23328  fincmp  23341  cmpsublem  23347  cmpsub  23348  uncmp  23351  hauscmplem  23354  dfconn2  23367  iunconnlem  23375  unconn  23377  is1stc2  23390  1stcrest  23401  1stcelcls  23409  llyi  23422  nllyi  23423  subislly  23429  lly1stc  23444  txcnp  23568  txcnmpt  23572  hausdiag  23593  kqcldsat  23681  isfbas2  23783  isfil2  23804  fbasfip  23816  elfg  23819  filconn  23831  rnelfmlem  23900  rnelfm  23901  fmfnfmlem2  23903  fmfnfmlem4  23905  fmfnfm  23906  flimrest  23931  hauspwpwf1  23935  fclsrest  23972  alexsubALTlem2  23996  alexsubALTlem3  23997  alexsubALTlem4  23998  alexsubALT  23999  istmd  24022  istgp  24025  tsmssubm  24091  tsmssplit  24100  istrg  24112  istdrg  24114  istlm  24133  ustfilxp  24161  utoptop  24183  utop3cls  24200  bldisj  24348  blin  24371  blres  24381  lpbl  24456  metrest  24477  restmetu  24523  isngp  24549  isnlm  24636  isnmhm  24707  xrtgioo  24766  xrsmopn  24772  icccmplem2  24783  reconnlem2  24787  icoopnst  24907  iocopnst  24908  bndth  24928  zclmncvs  25120  isncvsngp  25121  ncvsprp  25124  ncvsm1  25126  ncvsdif  25127  ncvspi  25128  ncvs1  25129  ncvspds  25133  iscph  25142  tcphcph  25209  cfilfcls  25246  cmetcaulem  25260  isbn  25310  cldcss2  25414  hlhil  25415  ovolfcl  25439  ovolicc2lem2  25491  ovolicc2  25495  shftmbl  25511  volfiniun  25520  mbfmax  25622  mbfimaopnlem  25628  mbfaddlem  25633  i1faddlem  25666  i1fmullem  25667  i1fres  25679  itg1climres  25688  mbfi1fseqlem4  25692  itg2splitlem  25722  itg2split  25723  itgresr  25752  ellimc2  25850  ellimc3  25852  limcun  25868  dvreslem  25882  dvne0  25988  itgsubstlem  26027  ig1pval3  26157  aaliou2  26320  aaliou2b  26321  pilem1  26433  rlimcnp2  26943  fsumharmonic  26989  ppisval2  27082  prmorcht  27155  fsumvma2  27192  pclogsum  27193  vmasum  27194  chpchtsum  27197  chpub  27198  rpvmasum2  27490  madeval2  27826  tglineineq  28519  trlsegvdeg  30109  frgrncvvdeqlem7  30187  frgrncvvdeqlem9  30189  minvecolem1  30756  minvecolem4a  30759  minvecolem4b  30760  minvecolem4  30762  h2hcau  30861  axhcompl-zf  30880  hhcmpl  31082  hhcms  31085  ocin  31178  ocnel  31180  shmodsi  31271  pjhthlem2  31274  omlsilem  31284  pjoc1i  31313  spansnm0i  31532  nonbooli  31533  5oalem7  31542  3oalem3  31546  pjssmii  31563  mayete3i  31610  nmcopex  31911  nmcoplb  31912  lncnopbd  31919  nmcfnex  31935  nmcfnlb  31936  riesz4  31946  riesz1  31947  riesz2  31948  cnlnadjlem3  31951  cnlnadjlem5  31953  cnlnadjlem9  31957  cnlnadjeu  31960  rnbra  31989  pjimai  32058  pjclem4a  32080  pj3lem1  32088  jpi  32152  sumdmdii  32297  sumdmdlem  32300  sumdmdlem2  32301  cdjreui  32314  cdj3lem1  32316  iunin1f  32427  disjorf  32448  ofpreima  32532  1stpreima  32568  2ndpreima  32569  iocinioc2  32629  ssnnssfz  32637  cntzun  32864  isorng  33113  kerunit  33133  prmidl0  33262  ressply1mon1p  33380  ccfldextdgrr  33491  crefdf  33580  cmpcref  33582  cmppcmp  33590  cnre2csqima  33643  ordtconnlem1  33656  lmxrge0  33684  isrrext  33732  esum0  33799  esumcst  33813  esumpcvgval  33828  esumcvg  33836  measvuni  33964  eulerpartlemt0  34120  eulerpartlemr  34125  eulerpartlemgf  34130  eulerpartlemgs2  34131  eulerpartlemn  34132  fiblem  34149  oddprm2  34418  bnj1173  34764  bnj1174  34765  bnj1279  34780  elima4  35502  dfon2lem4  35513  ellimits  35637  dfom5b  35639  brapply  35665  brcap  35667  dfrecs2  35677  dfrdg4  35678  finminlem  35933  neibastop2lem  35975  neibastop2  35976  neifg  35986  tailfb  35992  onsucconni  36052  onintopssconn  36055  onsucsuccmpi  36058  limsucncmpi  36060  onint1  36064  bj-inrab  36536  bj-rcleqf  36635  bj-restuni  36707  bj-opelresdm  36755  bj-idres  36770  bj-opelidres  36771  bj-eldiag  36786  bj-eldiag2  36787  bj-ccinftydisj  36823  taupilem3  36929  isbasisrelowllem1  36965  isbasisrelowllem2  36966  nlpineqsn  37018  fvineqsneu  37021  ptrest  37223  poimirlem29  37253  poimirlem30  37254  mblfinlem2  37262  mbfposadd  37271  itg2gt0cn  37279  dvasin  37308  inixp  37332  0totbnd  37377  sstotbnd3  37380  heibor1lem  37413  heibor1  37414  heiborlem6  37420  isexid2  37459  smgrpismgmOLD  37466  issmgrpOLD  37467  mndoissmgrpOLD  37472  ismndo  37476  exidresid  37483  rngo1cl  37543  isfld2  37609  ralin  37850  ineleq  37956  refressn  38045  eleccossin  38085  elrefsymrelsrel  38173  dfeldisj3  38321  disjlem14  38400  prtlem14  38476  lshpdisj  38589  lkrin  38766  ishlat1  38954  pmodlem2  39450  pclfinN  39503  pclcmpatN  39504  osumcllem4N  39562  pexmidlem1N  39573  dihmeetlem1N  40893  dihglblem5apreN  40894  dihmeetlem4preN  40909  dihmeetlem13N  40922  dochnel2  40995  lcdlss  41222  mapd1o  41251  baerlem3lem2  41313  baerlem5alem2  41314  baerlem5blem2  41315  cmpfiiin  42259  mrefg2  42269  fz1eqin  42331  fnwe2lem2  42617  islmodfg  42635  islssfg2  42637  lnr2i  42682  rp-fakeinunass  43087  fiinfi  43145  elinintab  43147  elinintrab  43149  elinlem  43170  cnvcnvintabd  43172  ntrneikb  43666  ntrneik3  43668  ntrneik13  43670  ismnushort  43880  radcnvrat  43893  nzin  43897  onfrALTlem2  44127  onfrALTlem2VD  44470  iooabslt  45022  iccintsng  45046  lptioo2cn  45171  lptioo1cn  45172  cncfuni  45412  icccncfext  45413  stoweidlem44  45570  fourierdlem42  45675  fourierdlem80  45712  sge00  45902  eldmressn  46557  afvres  46690  afv2res  46757  prproropf1olem0  46979  31prm  47074  rngccatidALTV  47520  rhmsubcALTVlem3  47531  funcringcsetcALTV2lem7  47544  ringccatidALTV  47554  ringcbasbasALTV  47560  funcringcsetclem7ALTV  47567  fldhmsubcALTV  47581  ssnn0ssfz  47599  elbigo2  47811  itsclinecirc0in  48034  opndisj  48107  clddisj  48108  i0oii  48124  io1ii  48125