Theorem elin 3920

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 3474	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ V)
2		elex 3474	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	adantl 485	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2849	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2849	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 641	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 3911	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3639	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 380	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

Syntax hints:   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141  Vcvv 3453   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-in 3911

This theorem is referenced by:  elini  4151  elind  4152  elinel1  4153  elinel2  4154  elin2  4155  elin3  4158  ineqri  4164  nfin  4176  inass  4179  ssin  4190  ssrin  4193  ralin  4201  rexin  4202  dfss4  4221  difin  4224  indi  4236  undi  4237  unineq  4240  indifdi  4246  difin2  4253  inrab2  4269  ndisj  4322  inn0f  4323  difin0ss  4325  inssdif0  4326  inelcm  4418  inundif  4432  elinsn  4668  uniinOLD  4889  intun  4937  intprg  4938  elrint  4946  iunin2  5027  iinin2  5034  elriin  5037  disjor  5081  disjiun  5087  brin  5151  trin  5218  inex1  5272  inuni  5305  wefrc  5639  inopab  5800  inxp  5802  dmin  5885  dfres3  5968  intasym  6097  asymref  6098  dminss  6133  imainss  6134  inimasn  6136  cnvresima  6211  dfco2a  6227  ordtri3or  6372  2elresin  6636  respreima  7041  fvcofneq  7068  tpres  7179  isomin  7315  isoini  7316  offval  7663  ordpwsuc  7789  frpoins3xpg  8113  frpoins3xp3g  8114  xpord3pred  8125  ressuppss  8156  frrlem13  8272  fprlem1  8274  uniinqs  8772  mapval2  8848  ixpin  8899  boxriin  8916  disjen  9100  ssenen  9117  onfin2  9179  elfpw  9292  fiin  9363  inf3lem2  9579  epfrs  9681  cp  9844  dfac5lem1  10074  dfac5lem5  10078  dfac5  10080  kmlem3  10104  kmlem14  10115  kmlem15  10116  fin23lem26  10277  pwxpndom2  10618  ingru  10768  gruina  10771  grur1  10773  axgroth4  10785  grothprim  10787  ixxdisj  13359  icodisj  13475  fzdisj  13551  nn0disj  13644  fzouzdisj  13696  cotr2g  14984  limsupgle  15485  ello12  15524  elo12  15535  lo1resb  15572  rlimresb  15573  o1resb  15574  lo1eq  15576  rlimeq  15577  fsumsplit  15749  sumsplit  15776  fsum2dlem  15778  fprod2dlem  15991  bitsmod  16451  saddisjlem  16479  sadadd  16482  sadass  16486  smuval2  16497  smupval  16503  smueqlem  16505  smumul  16508  isprm7  16724  prmreclem5  16937  prmrec  16939  4sqlem12  16973  vdwmc  16995  setsstruct2  17191  acsfn  17672  iszeroo  18012  iszeroi  18023  fpwipodrs  18553  psss  18593  insubm  18833  subgacs  19183  nsgacs  19184  resscntz  19354  gsmsymgreq  19453  sylow2a  19640  lsmmod  19696  lsmdisj2  19703  gsumzsplit  19948  subgdmdprd  20057  dprdcntz2  20061  dprddisj2  20062  pgpfac1lem3  20100  rnghmval2  20470  isrhm  20504  subsubrng2  20591  subsubrg2  20626  rnghmsubcsetclem1  20658  funcrngcsetcALT  20668  zrinitorngc  20669  zrtermorngc  20670  rhmsubcsetclem1  20687  rhmsubcrngclem1  20693  ringcbasbas  20700  zrtermoringc  20702  srhmsubclem1  20704  fldhmsubc  20812  acsfn1p  20826  subrgacs  20827  sdrgacs  20828  isorng  20888  lssacs  21012  lspdisj  21173  lspdisjb  21174  dfprm2  21503  irinitoringc  21509  ocvin  21704  unocv  21710  iunocv  21711  obselocv  21758  isassa  21886  aspid  21904  aspval2  21928  pmatcoe1fsupp  22739  isbasis2g  22986  tgval2  22994  tgcl  23007  ppttop  23045  epttop  23047  ssntr  23096  ntreq0  23115  isclo  23125  restntr  23220  restlp  23221  cnpresti  23326  cnprest  23327  cnprest2  23328  lmss  23336  haust1  23390  nrmsep3  23393  isnrm2  23396  lmmo  23418  fincmp  23431  cmpsublem  23437  cmpsub  23438  uncmp  23441  hauscmplem  23444  dfconn2  23457  iunconnlem  23465  unconn  23467  is1stc2  23480  1stcrest  23491  1stcelcls  23499  llyi  23512  nllyi  23513  subislly  23519  lly1stc  23534  txcnp  23658  txcnmpt  23662  hausdiag  23683  kqcldsat  23771  isfbas2  23873  isfil2  23894  fbasfip  23906  elfg  23909  filconn  23921  rnelfmlem  23990  rnelfm  23991  fmfnfmlem2  23993  fmfnfmlem4  23995  fmfnfm  23996  flimrest  24021  hauspwpwf1  24025  fclsrest  24062  alexsubALTlem2  24086  alexsubALTlem3  24087  alexsubALTlem4  24088  alexsubALT  24089  istmd  24112  istgp  24115  tsmssubm  24181  tsmssplit  24190  istrg  24202  istdrg  24204  istlm  24223  ustfilxp  24251  utoptop  24272  utop3cls  24289  bldisj  24436  blin  24459  blres  24469  lpbl  24541  metrest  24562  restmetu  24608  isngp  24634  isnlm  24713  isnmhm  24784  xrtgioo  24845  xrsmopn  24851  icccmplem2  24862  reconnlem2  24866  icoopnst  24979  iocopnst  24980  bndth  24998  zclmncvs  25188  isncvsngp  25189  ncvsprp  25192  ncvsm1  25194  ncvsdif  25195  ncvspi  25196  ncvs1  25197  ncvspds  25201  iscph  25210  tcphcph  25277  cfilfcls  25314  cmetcaulem  25328  isbn  25378  cldcss2  25482  hlhil  25483  ovolfcl  25506  ovolicc2lem2  25558  ovolicc2  25562  shftmbl  25578  volfiniun  25587  mbfmax  25689  mbfimaopnlem  25695  mbfaddlem  25700  i1faddlem  25733  i1fmullem  25734  i1fres  25745  itg1climres  25754  mbfi1fseqlem4  25758  itg2splitlem  25788  itg2split  25789  itgresr  25819  ellimc2  25917  ellimc3  25919  limcun  25935  dvreslem  25949  dvne0  26051  itgsubstlem  26088  ig1pval3  26216  aaliou2  26379  aaliou2b  26380  pilem1  26489  rlimcnp2  27006  fsumharmonic  27051  ppisval2  27144  prmorcht  27217  fsumvma2  27253  pclogsum  27254  vmasum  27255  chpchtsum  27258  chpub  27259  rpvmasum2  27551  madeval2  27901  tglineineq  28787  trlsegvdeg  30373  frgrncvvdeqlem7  30451  frgrncvvdeqlem9  30453  minvecolem1  31021  minvecolem4a  31024  minvecolem4b  31025  minvecolem4  31027  h2hcau  31126  axhcompl-zf  31145  hhcmpl  31347  hhcms  31350  ocin  31443  ocnel  31445  shmodsi  31536  pjhthlem2  31539  omlsilem  31549  pjoc1i  31578  spansnm0i  31797  nonbooli  31798  5oalem7  31807  3oalem3  31811  pjssmii  31828  mayete3i  31875  nmcopex  32176  nmcoplb  32177  lncnopbd  32184  nmcfnex  32200  nmcfnlb  32201  riesz4  32211  riesz1  32212  riesz2  32213  cnlnadjlem3  32216  cnlnadjlem5  32218  cnlnadjlem9  32222  cnlnadjeu  32225  rnbra  32254  pjimai  32323  pjclem4a  32345  pj3lem1  32353  jpi  32417  sumdmdii  32562  sumdmdlem  32565  sumdmdlem2  32566  cdjreui  32579  cdj3lem1  32581  iunin1f  32704  disjorf  32726  ofpreima  32815  1stpreima  32857  2ndpreima  32858  iocinioc2  32929  ssnnssfz  32937  cntzun  33218  kerunit  33470  prmidl0  33596  ressply1mon1p  33723  ccfldextdgrr  33928  crefdf  34104  cmpcref  34106  cmppcmp  34114  cnre2csqima  34167  ordtconnlem1  34180  lmxrge0  34208  isrrext  34256  esum0  34305  esumcst  34319  esumpcvgval  34334  esumcvg  34342  measvuni  34470  eulerpartlemt0  34625  eulerpartlemr  34630  eulerpartlemgf  34635  eulerpartlemgs2  34636  eulerpartlemn  34637  fiblem  34654  oddprm2  34911  bnj1173  35259  bnj1174  35260  bnj1279  35275  elima4  36079  dfon2lem4  36087  ellimits  36211  dfom5b  36213  brapply  36239  brcap  36241  dfrecs2  36253  dfrdg4  36254  finminlem  36631  neibastop2lem  36673  neibastop2  36674  neifg  36684  tailfb  36690  onsucconni  36750  onintopssconn  36753  onsucsuccmpi  36756  limsucncmpi  36758  onint1  36762  mh-infprim2bi  36860  bj-inrab  37365  bj-rcleqf  37463  bj-restuni  37540  bj-opelresdm  37590  bj-idres  37605  bj-opelidres  37606  bj-eldiag  37621  bj-eldiag2  37622  bj-ccinftydisj  37658  taupilem3  37764  isbasisrelowllem1  37802  isbasisrelowllem2  37803  nlpineqsn  37855  fvineqsneu  37858  ptrest  38071  poimirlem29  38101  poimirlem30  38102  mblfinlem2  38110  mbfposadd  38119  itg2gt0cn  38127  dvasin  38156  inixp  38180  0totbnd  38225  sstotbnd3  38228  heibor1lem  38261  heibor1  38262  heiborlem6  38268  isexid2  38307  smgrpismgmOLD  38314  issmgrpOLD  38315  mndoissmgrpOLD  38320  ismndo  38324  exidresid  38331  rngo1cl  38391  isfld2  38457  ineleq  38806  refressn  38985  eleccossin  39025  elrefsymrelsrel  39107  dfeldisj3  39263  eldisjdmqsim  39269  disjlem14  39353  prtlem14  39451  lshpdisj  39564  lkrin  39741  ishlat1  39929  pmodlem2  40424  pclfinN  40477  pclcmpatN  40478  osumcllem4N  40536  pexmidlem1N  40547  dihmeetlem1N  41867  dihglblem5apreN  41868  dihmeetlem4preN  41883  dihmeetlem13N  41896  dochnel2  41969  lcdlss  42196  mapd1o  42225  baerlem3lem2  42287  baerlem5alem2  42288  baerlem5blem2  42289  redvmptabs  42922  cmpfiiin  43231  mrefg2  43241  fz1eqin  43303  fnwe2lem2  43581  islmodfg  43599  islssfg2  43601  lnr2i  43646  rp-fakeinunass  44044  fiinfi  44102  elinintab  44104  elinintrab  44106  elinlem  44127  cnvcnvintabd  44129  ntrneikb  44623  ntrneik3  44625  ntrneik13  44627  ismnushort  44830  radcnvrat  44843  nzin  44847  onfrALTlem2  45075  onfrALTlem2VD  45417  relpmin  45481  pwclaxpow  45513  dfac5prim  45519  modelac8prim  45521  permac8prim  45543  iooabslt  46028  iccintsng  46052  lptioo2cn  46172  lptioo1cn  46173  cncfuni  46413  icccncfext  46414  stoweidlem44  46571  fourierdlem42  46676  fourierdlem80  46713  sge00  46903  eldmressn  47584  afvres  47719  afv2res  47786  prproropf1olem0  48061  31prm  48159  indprmfz  48192  rngccatidALTV  48847  rhmsubcALTVlem3  48858  funcringcsetcALTV2lem7  48871  ringccatidALTV  48881  ringcbasbasALTV  48887  funcringcsetclem7ALTV  48894  fldhmsubcALTV  48908  ssnn0ssfz  48924  elbigo2  49127  itsclinecirc0in  49350  resinsnALT  49447  opndisj  49477  clddisj  49478  i0oii  49494  io1ii  49495