Theorem elin 4095

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 487	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ V)
4		eleq1 2851	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		eleq1 2851	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
6	4, 5	anbi12d 644	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
7		df-in 4093	. . 3 ⊢ (𝐵 ∩ 𝐶) = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)}
8	6, 7	elab2g 3636	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶)))
9	1, 3, 8	pm5.21nii 381	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2146  Vcvv 3453   ∩ cin 4091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-in 4093

This theorem is used by:  elini  4098  elind  4099  elinel1  4100  elinel2  4101  elin2  4102  elin3  4105  ineqri  4111  nfin  4123  inass  4126  ssin  4137  ssrin  4140  ralin  4148  rexin  4149  dfss4  4216  difin  4219  indi  4231  undi  4232  unineq  4235  indifdi  4241  difin2  4248  inrab2  4264  ndisj  4320  inn0f  4321  difin0ss  4323  inssdif0OLD  4325  inelcm  4420  inundif  4437  elinsn  4670  uniinOLD  4894  intun  4942  intprg  4943  elrint  4951  iunin2  5031  iinin2  5040  elriin  5043  disjor  5087  disjiun  5093  brin  5159  trin  5226  inex1  5280  inuni  5314  wefrc  5648  inopab  5811  inxp  5813  dmin  5897  dfres3  5979  intasym  6114  asymref  6115  dminss  6148  imainss  6149  inimasn  6151  cnvresima  6237  dfco2a  6253  ordtri3or  6401  2elresin  6668  respreima  7073  fvcofneq  7101  tpres  7214  isomin  7352  isoini  7353  offval  7709  ordpwsuc  7833  fnwe2lem3  8157  frpoins3xpg  8167  frpoins3xp3g  8168  xpord3pred  8179  ressuppss  8211  frrlem13  8327  fprlem1  8329  uniinqs  8829  mapval2  8911  ixpin  8962  boxriin  8979  disjen  9164  ssenen  9181  onfin2  9243  elfpw  9354  fiin  9424  inf3lem2  9640  epfrs  9742  cp  9964  dfac5lem1  10212  dfac5lem5  10216  dfac5  10217  kmlem3  10241  kmlem14  10252  kmlem15  10253  fin23lem26  10413  pwxpndom2  10760  ingru  10910  gruina  10913  grur1  10915  axgroth4  10927  grothprim  10929  ixxdisj  13501  icodisj  13617  fzdisj  13695  nn0disj  13788  fzouzdisj  13840  cotr2g  15141  limsupgle  15656  ello12  15695  elo12  15706  lo1resb  15743  rlimresb  15744  o1resb  15745  lo1eq  15747  rlimeq  15748  fsumsplit  15919  sumsplit  15946  fsum2dlem  15948  fprod2dlem  16159  bitsmod  16618  saddisjlem  16646  sadadd  16649  sadass  16653  smuval2  16664  smupval  16670  smueqlem  16672  smumul  16675  isprm7  16896  prmreclem5  17110  prmrec  17112  4sqlem12  17146  vdwmc  17168  setsstruct2  17364  acsfn  17845  iszeroo  18185  iszeroi  18196  fpwipodrs  18726  psss  18766  insubm  19026  subgacs  19383  nsgacs  19384  resscntz  19559  gsmsymgreq  19658  sylow2a  19845  lsmmod  19901  lsmdisj2  19908  gsumzsplit  20153  subgdmdprd  20262  dprdcntz2  20266  dprddisj2  20267  pgpfac1lem3  20305  rnghmval2  20686  isrhm  20721  subsubrng2  20828  subsubrg2  20863  rnghmsubcsetclem1  20895  funcrngcsetcALT  20905  zrinitorngc  20906  zrtermorngc  20907  rhmsubcsetclem1  20924  rhmsubcrngclem1  20930  ringcbasbas  20937  zrtermoringc  20939  srhmsubclem1  20941  fldhmsubc  21054  acsfn1p  21068  subrgacs  21069  sdrgacs  21070  isorng  21130  lssacs  21254  lspdisj  21415  lspdisjb  21416  prmidl0  21646  dfprm2  21791  irinitoringc  21797  ocvin  21992  unocv  21998  iunocv  21999  obselocv  22046  isassa  22176  aspid  22194  aspval2  22218  pmatcoe1fsupp  23031  isbasis2g  23278  tgval2  23286  tgcl  23299  ppttop  23337  epttop  23339  ssntr  23388  ntreq0  23407  isclo  23417  restntr  23512  restlp  23513  cnpresti  23618  cnprest  23619  cnprest2  23620  lmss  23628  haust1  23682  nrmsep3  23685  isnrm2  23688  lmmo  23710  fincmp  23723  cmpsublem  23729  cmpsub  23730  uncmp  23733  hauscmplem  23736  dfconn2  23749  iunconnlem  23757  unconn  23759  is1stc2  23772  1stcrest  23783  1stcelcls  23792  llyi  23805  nllyi  23806  subislly  23812  lly1stc  23827  txcnp  23951  txcnmpt  23955  hausdiag  23976  kqcldsat  24064  isfbas2  24166  isfil2  24187  fbasfip  24199  elfg  24202  filconn  24214  rnelfmlem  24283  rnelfm  24284  fmfnfmlem2  24286  fmfnfmlem4  24288  fmfnfm  24289  flimrest  24314  hauspwpwf1  24318  fclsrest  24355  alexsubALTlem2  24379  alexsubALTlem3  24380  alexsubALTlem4  24381  alexsubALT  24382  istmd  24405  istgp  24408  tsmssubm  24474  tsmssplit  24483  istrg  24495  istdrg  24497  istlm  24516  ustfilxp  24544  utoptop  24565  utop3cls  24582  bldisj  24729  blin  24752  blres  24762  lpbl  24834  metrest  24855  restmetu  24901  isngp  24927  isnlm  25006  isnmhm  25077  xrtgioo  25138  xrsmopn  25144  icccmplem2  25155  reconnlem2  25159  icoopnst  25272  iocopnst  25273  bndth  25291  zclmncvs  25481  isncvsngp  25482  ncvsprp  25485  ncvsm1  25487  ncvsdif  25488  ncvspi  25489  ncvs1  25490  ncvspds  25494  iscph  25503  tcphcph  25570  cfilfcls  25607  cmetcaulem  25621  isbn  25671  cldcss2  25775  hlhil  25776  ovolfcl  25799  ovolicc2lem2  25851  ovolicc2  25855  shftmbl  25871  volfiniun  25880  mbfmax  25982  mbfimaopnlem  25988  mbfaddlem  25993  i1faddlem  26026  i1fmullem  26027  i1fres  26038  itg1climres  26047  mbfi1fseqlem4  26051  itg2splitlem  26081  itg2split  26082  itgresr  26111  ellimc2  26209  ellimc3  26211  limcun  26227  dvreslem  26241  dvne0  26343  itgsubstlem  26380  ig1pval3  26508  aaliou2  26679  aaliou2b  26680  pilem1  26790  rlimcnp2  27306  fsumharmonic  27351  ppisval2  27444  prmorcht  27517  fsumvma2  27553  pclogsum  27554  vmasum  27555  chpchtsum  27558  chpub  27559  rpvmasum2  27851  madeval2  28231  tglineineq  29123  angmgmaddcpbl  29402  trlsegvdeg  30840  frgrncvvdeqlem7  30918  frgrncvvdeqlem9  30920  minvecolem1  31488  minvecolem4a  31491  minvecolem4b  31492  minvecolem4  31494  h2hcau  31593  axhcompl-zf  31612  hhcmpl  31814  hhcms  31817  ocin  31910  ocnel  31912  shmodsi  32003  pjhthlem2  32006  omlsilem  32016  pjoc1i  32045  spansnm0i  32264  nonbooli  32265  5oalem7  32274  3oalem3  32278  pjssmii  32295  mayete3i  32342  nmcopex  32643  nmcoplb  32644  lncnopbd  32651  nmcfnex  32667  nmcfnlb  32668  riesz4  32678  riesz1  32679  riesz2  32680  cnlnadjlem3  32683  cnlnadjlem5  32685  cnlnadjlem9  32689  cnlnadjeu  32692  rnbra  32721  pjimai  32790  pjclem4a  32812  pj3lem1  32820  jpi  32884  sumdmdii  33029  sumdmdlem  33032  sumdmdlem2  33033  cdjreui  33046  cdj3lem1  33048  iunin1f  33206  disjorf  33227  ofpreima  33313  1stpreima  33354  2ndpreima  33355  iocinioc2  33424  ssnnssfz  33432  cntzun  33693  kerunit  33939  ressply1mon1p  34153  ccfldextdgrr  34357  crefdf  34533  cmppcmp  34543  cnre2csqima  34596  ordtconnlem1  34609  lmxrge0  34637  isrrext  34685  esum0  34734  esumcst  34748  esumpcvgval  34763  esumcvg  34771  measvuni  34900  eulerpartlemt0  35054  eulerpartlemr  35059  eulerpartlemgf  35064  eulerpartlemgs2  35065  eulerpartlemn  35066  fiblem  35083  oddprm2  35337  bnj1173  35685  bnj1174  35686  bnj1279  35701  elima4  36667  dfon2lem4  36675  ellimits  36799  dfom5b  36801  brapply  36827  brcap  36829  dfrecs2  36841  dfrdg4  36842  finminlem  37233  neibastop2lem  37275  neibastop2  37276  neifg  37286  tailfb  37292  onsucconni  37352  onintopssconn  37355  onsucsuccmpi  37358  limsucncmpi  37360  onint1  37364  mh-infprim2bi  37462  bj-inex1gALT  37964  bj-inrab  37967  bj-rcleqf  38065  bj-elinxp  38087  bj-restuni  38157  bj-opelresdm  38206  bj-idres  38221  bj-opelidres  38222  bj-eldiag  38237  bj-eldiag2  38238  bj-ccinftydisj  38274  taupilem3  38380  isbasisrelowllem1  38418  isbasisrelowllem2  38419  nlpineqsn  38471  fvineqsneu  38474  ptrest  38677  poimirlem29  38707  poimirlem30  38708  mblfinlem2  38716  mbfposadd  38725  itg2gt0cn  38733  dvasin  38762  inixp  38802  0totbnd  38847  sstotbnd3  38850  heibor1lem  38883  heibor1  38884  heiborlem6  38890  isexid2  38929  smgrpismgmOLD  38936  issmgrpOLD  38937  mndoissmgrpOLD  38942  ismndo  38946  exidresid  38953  rngo1cl  39013  isfld2  39079  ineleq  39426  refressn  39605  eleccossin  39645  elrefsymrelsrel  39727  dfeldisj3  39883  eldisjdmqsim  39889  disjlem14  39973  prtlem14  40071  lshpdisj  40184  lkrin  40361  ishlat1  40549  pmodlem2  41044  pclfinN  41097  pclcmpatN  41098  osumcllem4N  41156  pexmidlem1N  41167  dihmeetlem1N  42487  dihglblem5apreN  42488  dihmeetlem4preN  42503  dihmeetlem13N  42516  dochnel2  42589  lcdlss  42816  mapd1o  42845  baerlem3lem2  42907  baerlem5alem2  42908  baerlem5blem2  42909  redvmptabs  43551  cmpfiiin  43848  mrefg2  43858  fz1eqin  43920  islmodfg  44211  islssfg2  44213  lnr2i  44258  rp-fakeinunass  44656  fiinfi  44714  elinintab  44716  elinintrab  44718  elinlem  44738  cnvcnvintabd  44740  ntrneikb  45234  ntrneik3  45236  ntrneik13  45238  ismnushort  45425  radcnvrat  45438  nzin  45442  onfrALTlem2  45668  onfrALTlem2VD  46010  relpmin  46081  pwclaxpow  46113  dfac5prim  46119  modelac8prim  46121  permac8prim  46143  iooabslt  46650  iccintsng  46674  lptioo2cn  46794  lptioo1cn  46795  cncfuni  47035  icccncfext  47036  stoweidlem44  47193  fourierdlem42  47298  fourierdlem80  47335  sge00  47525  wrddin2  48037  chndin2  48042  chnrin2  48047  eldmressn  48246  afvres  48381  afv2res  48448  prproropf1olem0  48723  31prm  48821  indprmfz  48854  rngccatidALTV  49508  rhmsubcALTVlem3  49519  funcringcsetcALTV2lem7  49532  ringccatidALTV  49542  ringcbasbasALTV  49548  funcringcsetclem7ALTV  49555  fldhmsubcALTV  49569  dfidom2  49579  ssnn0ssfz  49600  elbigo2  49803  itsclinecirc0in  50026  resinsnALT  50125  opndisj  50156  clddisj  50157  i0oii  50173  io1ii  50174