Theorem elin 3608

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	|- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )

Proof of Theorem elin

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3040	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 3040	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 473	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2537	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2537	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
6	4, 5	anbi12d 725	. . 3 |- ( x = A -> ( ( x e. B /\ x e. C ) <-> ( A e. B /\ A e. C ) ) )
7		df-in 3397	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 3175	. 2 |- ( A e. _V -> ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) ) )
9	1, 3, 8	pm5.21nii 360	1 |- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )

Syntax hints:   <-> wb 189   /\ wa 376   = wceq 1452   e. wcel 1904   _Vcvv 3031   i^i cin 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-in 3397

This theorem is referenced by:  elind  3609  elinel1  3610  elinel2  3611  elin2  3612  elin1d  3613  elin2d  3614  elin3  3615  incom  3616  ineqri  3617  ineq1  3618  inass  3633  inss1  3643  ssin  3645  ssrin  3648  dfss4  3668  difin  3671  indi  3680  undi  3681  unineq  3684  indifdir  3690  difin2  3696  inrab2  3707  difin0ss  3745  inssdif0  3746  inelcm  3823  inundif  3836  uniin  4210  intun  4258  intpr  4259  elrint  4267  iunin2  4333  iinin2  4339  elriin  4342  disjor  4380  disjiun  4386  brin  4445  trin  4500  inex1  4537  inuni  4563  wefrc  4833  inopab  4970  inxp  4972  dmin  5048  opelres  5116  eldmeldmressn  5151  intasym  5221  asymref  5222  dminss  5256  imainss  5257  inimasn  5259  ssrnres  5281  cnvresima  5331  dfco2a  5342  predel  5404  ordtri3or  5462  2elresin  5697  respreima  6024  fvcofneq  6045  tpres  6133  isomin  6246  isoini  6247  offval  6557  ordpwsuc  6661  ressuppss  6953  wfrlem5  7058  erdisj  7429  uniinqs  7461  mapval2  7519  ixpin  7565  boxriin  7582  disjen  7747  ssenen  7764  onfin2  7782  elfpw  7894  fiin  7954  inf3lem2  8152  epfrs  8233  cp  8380  bnd2  8382  dfac5lem1  8572  dfac5lem5  8576  dfac5  8577  kmlem3  8600  kmlem14  8611  kmlem15  8612  fin23lem26  8773  isfin1-3  8834  pwxpndom2  9108  ingru  9258  gruina  9261  grur1  9263  axgroth4  9275  grothprim  9277  ixxdisj  11675  icodisj  11783  fzdisj  11852  uzdisj  11893  nn0disj  11932  fzouzdisj  11981  xpcogend  13113  cotr2g  13115  limsupgle  13612  ello12  13657  elo12  13668  lo1resb  13705  rlimresb  13706  o1resb  13707  lo1eq  13709  rlimeq  13710  fsumsplit  13883  sumsplit  13906  fsum2dlem  13908  explecnv  14000  fprod2dlem  14111  bitsmod  14489  saddisjlem  14517  sadadd  14520  sadass  14524  smuval2  14535  smupval  14541  smueqlem  14543  smumul  14546  prmreclem5  14943  prmrec  14945  4sqlem12  14979  vdwmc  15007  acsfn  15643  iszeroo  15975  iszeroi  15982  isdrs2  16262  fpwipodrs  16488  psss  16538  subgacs  16930  nsgacs  16931  resscntz  17063  gsmsymgreq  17151  sylow2a  17349  lsmmod  17403  lsmdisj2  17410  gsumzsplit  17638  subgdmdprd  17745  dprdcntz2  17749  dprddisj2  17750  pgpfac1lem3  17788  isrhm  18027  subsubrg2  18113  lssacs  18268  lspdisj  18426  lspdisjb  18427  isassa  18616  aspid  18631  aspval2  18648  dfprm2  19142  ocvin  19314  unocv  19320  iunocv  19321  obselocv  19368  pmatcoe1fsupp  19802  isbasis2g  20040  tgval2  20048  tgcl  20062  ppttop  20099  epttop  20101  clsval2  20142  ssntr  20150  ntreq0  20170  isclo  20180  restntr  20275  restlp  20276  cnpresti  20381  cnprest  20382  cnprest2  20383  lmss  20391  haust1  20445  nrmsep3  20448  isnrm2  20451  lmmo  20473  fincmp  20485  0cmp  20486  discmp  20490  cmpsublem  20491  cmpsub  20492  uncmp  20495  hauscmplem  20498  dfcon2  20511  iunconlem  20519  uncon  20521  is1stc2  20534  1stcrest  20545  1stcelcls  20553  llyi  20566  nllyi  20567  subislly  20573  lly1stc  20588  comppfsc  20624  txcnp  20712  txcnmpt  20716  hausdiag  20737  kqcldsat  20825  ptcmpfi  20905  isfbas2  20928  isfil2  20949  fbasfip  20961  elfg  20964  filcon  20976  rnelfmlem  21045  rnelfm  21046  fmfnfmlem2  21048  fmfnfmlem4  21050  fmfnfm  21051  flimrest  21076  hauspwpwf1  21080  fclsrest  21117  alexsubALTlem2  21141  alexsubALTlem3  21142  alexsubALTlem4  21143  alexsubALT  21144  ptcmp  21151  istmd  21167  istgp  21170  tsmssubm  21235  tsmssplit  21244  istrg  21256  istdrg  21258  istlm  21277  ustfilxp  21305  utoptop  21327  utop3cls  21344  bldisj  21491  blin  21514  blin2  21522  blres  21524  lpbl  21596  metrest  21617  restmetu  21663  isngp  21688  isnlm  21756  isnmhm  21845  xrtgioo  21902  xrsmopn  21908  icccmplem2  21919  reconnlem2  21923  icoopnst  22045  iocopnst  22046  bndth  22064  iscph  22226  tchcph  22289  cfilfcls  22322  cmetcaulem  22336  cmetss  22362  isbn  22384  cldcss2  22474  hlhil  22475  ovolfcl  22497  ovolicc1  22547  ovolicc2lem2  22549  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  ovolicc2lem5  22553  ovolicc2  22554  shftmbl  22570  volfiniun  22579  ioorf  22604  ioorfOLD  22609  mbfmax  22684  mbfimaopnlem  22690  mbfaddlem  22695  mbfadd  22696  mbfsub  22697  i1faddlem  22730  i1fmullem  22731  i1fres  22742  itg1climres  22751  mbfi1fseqlem4  22755  mbfmul  22763  itg2splitlem  22785  itg2split  22786  itgresr  22815  bddmulibl  22875  ellimc2  22911  ellimc3  22913  limcun  22929  dvreslem  22943  dvne0  23042  itgsubstlem  23079  ig1pval3  23205  ig1pval3OLD  23211  aaliou2  23375  aaliou2b  23376  pilem1  23485  rlimcnp2  23971  fsumharmonic  24016  ppisval2  24110  prmorcht  24184  fsumvma2  24221  pclogsum  24222  vmasum  24223  chpchtsum  24226  chpub  24227  chebbnd1lem1  24386  rpvmasum2  24429  tglineineq  24767  frgrancvvdeqlem4  25840  frgrancvvdeqlem7  25843  frgrancvvdeqlemA  25844  frgrancvvdeqlemC  25846  issubgo  26112  isexid2  26134  smgrpismgmOLD  26141  smgrpisass  26142  issmgrpOLD  26143  mndoissmgrpOLD  26148  mndoisexid  26149  ismndo  26152  rngo1cl  26238  minvecolem1  26597  minvecolem4a  26600  minvecolem4b  26601  minvecolem4  26603  minvecolem4aOLD  26610  minvecolem4bOLD  26611  minvecolem4OLD  26613  h2hcau  26713  axhcompl-zf  26732  hhcmpl  26934  hhcms  26937  ocin  27030  ocnel  27032  shmodsi  27123  pjhthlem2  27126  omlsilem  27136  pjoc1i  27165  spansnm0i  27384  nonbooli  27385  5oalem7  27394  3oalem3  27398  pjssmii  27415  mayete3i  27462  nmcopex  27763  nmcoplb  27764  lncnopbd  27771  nmcfnex  27787  nmcfnlb  27788  riesz4  27798  riesz1  27799  riesz2  27800  cnlnadjlem3  27803  cnlnadjlem5  27805  cnlnadjlem9  27809  cnlnadjeu  27812  rnbra  27841  pjimai  27910  pjclem4a  27932  pj3lem1  27940  jpi  28004  sumdmdii  28149  sumdmdlem  28152  sumdmdlem2  28153  cdjreui  28166  cdj3lem1  28168  iunin1f  28249  disjorf  28266  ofpreima  28343  1stpreima  28362  2ndpreima  28363  iocinioc2  28436  ssnnssfz  28442  isorng  28636  kerunit  28660  crefdf  28749  cmpcref  28751  cmppcmp  28759  pcmplfin  28761  cnre2csqima  28791  ordtconlem1  28804  lmxrge0  28832  isrrext  28878  esum0  28944  esumcst  28958  esumpcvgval  28973  esumcvg  28981  measvuni  29110  eulerpartlemt0  29275  eulerpartlemr  29280  eulerpartlemgf  29285  eulerpartlemgs2  29286  eulerpartlemn  29287  sseqf  29298  fiblem  29304  bnj521  29617  bnj1172  29882  bnj1173  29883  bnj1174  29884  bnj1279  29899  dfres3  30470  elima4  30492  dfon2lem4  30503  frrlem5  30589  ellimits  30748  dfom5b  30750  brapply  30776  brcap  30778  dfrecs2  30788  dfrdg4  30789  finminlem  31045  neibastop2lem  31087  neibastop2  31088  neifg  31098  tailfb  31104  onsucconi  31168  onintopsscon  31171  onsucsuccmpi  31174  limsucncmpi  31176  onint1  31180  bj-inrab  31598  bj-eldiag  31716  bj-eldiag2  31717  bj-ccinftydisj  31725  taupilem3  31790  isbasisrelowllem1  31828  isbasisrelowllem2  31829  ptrest  32003  poimirlem29  32033  poimirlem30  32034  mblfinlem2  32042  mbfposadd  32052  itg2gt0cn  32061  dvasin  32092  inixp  32119  0totbnd  32169  sstotbnd3  32172  heibor1lem  32205  heibor1  32206  heiborlem6  32212  exidresid  32241  isfld2  32302  prtlem14  32510  lshpdisj  32624  lkrin  32801  ishlat1  32989  pmodlem2  33483  pclfinN  33536  pclcmpatN  33537  osumcllem4N  33595  pexmidlem1N  33606  dihmeetlem1N  34929  dihglblem5apreN  34930  dihmeetlem4preN  34945  dihmeetlem13N  34958  dochnel2  35031  lcdlss  35258  mapd1o  35287  baerlem3lem2  35349  baerlem5alem2  35350  baerlem5blem2  35351  cmpfiiin  35610  mrefg2  35620  fz1eqin  35682  fnwe2lem2  35980  islmodfg  35998  islssfg2  36000  lnr2i  36046  acsfn1p  36136  subrgacs  36137  sdrgacs  36138  rp-fakeinunass  36231  fiinfi  36248  elinintab  36252  elinintrab  36254  elinlem  36275  cnvcnvintabd  36277  ndisj  36435  isprm7  36730  radcnvrat  36733  nzin  36737  onfrALTlem2  36982  onfrALTlem2VD  37349  elini  37440  inn0f  37476  iooabslt  37692  iccintsng  37720  lptioo2cn  37823  lptioo1cn  37824  cncfuni  37861  icccncfext  37862  stoweidlem44  38017  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem80  38162  sge00  38332  eldmressn  38769  afvres  38819  trlsegvdeg  40139  rnghmval2  40403  rnghmsubcsetclem1  40485  rngccatidALTV  40499  funcrngcsetcALT  40509  zrinitorngc  40510  zrtermorngc  40511  rhmsubcsetclem1  40531  rhmsubcrngclem1  40537  ringcbasbas  40544  funcringcsetcALTV2lem7  40552  ringccatidALTV  40562  ringcbasbasALTV  40568  funcringcsetclem7ALTV  40575  irinitoringc  40579  zrtermoringc  40580  srhmsubclem1  40583  fldhmsubc  40594  srhmsubcALTVlem1  40602  fldhmsubcALTV  40613  rhmsubcALTVlem3  40617  ssnn0ssfz  40638  elbigo2  40871