Theorem elin 4096

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ∩ cin 4092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094

This theorem is used by:  elini  4099  elind  4100  elinel1  4101  elinel2  4102  elin2  4103  elin3  4106  ineqri  4112  nfin  4124  inass  4127  ssin  4138  ssrin  4141  ralin  4149  rexin  4150  dfss4  4217  difin  4220  indi  4232  undi  4233  unineq  4236  indifdi  4242  difin2  4249  inrab2  4265  ndisj  4321  inn0f  4322  difin0ss  4324  inssdif0OLD  4326  inelcm  4421  inundif  4438  elinsn  4672  uniinOLD  4897  intun  4945  intprg  4946  elrint  4954  iunin2  5034  iinin2  5043  elriin  5046  disjor  5090  disjiun  5096  brin  5163  trin  5230  inex1  5284  inuni  5318  wefrc  5652  inopab  5817  inxp  5819  dmin  5905  dfres3  5991  intasym  6127  asymref  6128  dminss  6161  imainss  6162  inimasn  6164  cnvresima  6250  dfco2a  6266  ordtri3or  6421  2elresin  6690  respreima  7097  fvcofneq  7125  tpres  7238  isomin  7376  isoini  7377  offval  7734  ordpwsuc  7860  fnwe2lem3  8184  frpoins3xpg  8194  frpoins3xp3g  8195  xpord3pred  8206  ressuppss  8238  frrlem13  8354  fprlem1  8356  uniinqs  8856  mapval2  8938  ixpin  8989  boxriin  9006  disjen  9191  ssenen  9208  onfin2  9270  elfpw  9381  fiin  9451  inf3lem2  9667  epfrs  9769  cp  9991  dfac5lem1  10241  dfac5lem5  10245  dfac5  10246  kmlem3  10270  kmlem14  10281  kmlem15  10282  fin23lem26  10442  pwxpndom2  10789  ingru  10939  gruina  10942  grur1  10944  axgroth4  10956  grothprim  10958  ixxdisj  13531  icodisj  13647  fzdisj  13725  nn0disj  13818  fzouzdisj  13870  cotr2g  15172  limsupgle  15688  ello12  15727  elo12  15738  lo1resb  15775  rlimresb  15776  o1resb  15777  lo1eq  15779  rlimeq  15780  fsumsplit  15951  sumsplit  15978  fsum2dlem  15980  fprod2dlem  16191  bitsmod  16650  saddisjlem  16678  sadadd  16681  sadass  16685  smuval2  16696  smupval  16702  smueqlem  16704  smumul  16707  isprm7  16928  prmreclem5  17142  prmrec  17144  4sqlem12  17178  vdwmc  17200  setsstruct2  17396  acsfn  17883  iszeroo  18223  iszeroi  18234  fpwipodrs  18764  psss  18804  insubm  19064  subgacs  19421  nsgacs  19422  resscntz  19598  gsmsymgreq  19697  sylow2a  19884  lsmmod  19940  lsmdisj2  19947  gsumzsplit  20192  subgdmdprd  20301  dprdcntz2  20305  dprddisj2  20306  pgpfac1lem3  20344  rnghmval2  20725  isrhm  20760  subsubrng2  20867  subsubrg2  20902  rnghmsubcsetclem1  20934  funcrngcsetcALT  20944  zrinitorngc  20945  zrtermorngc  20946  rhmsubcsetclem1  20963  rhmsubcrngclem1  20969  ringcbasbas  20976  zrtermoringc  20978  srhmsubclem1  20980  fldhmsubc  21093  acsfn1p  21107  subrgacs  21108  sdrgacs  21109  isorng  21169  lssacs  21293  lspdisj  21454  lspdisjb  21455  prmidl0  21685  dfprm2  21834  irinitoringc  21840  ocvin  22035  unocv  22041  iunocv  22042  obselocv  22089  isassa  22219  aspid  22237  aspval2  22261  pmatcoe1fsupp  23074  isbasis2g  23321  tgval2  23329  tgcl  23342  ppttop  23380  epttop  23382  ssntr  23431  ntreq0  23450  isclo  23460  restntr  23555  restlp  23556  cnpresti  23661  cnprest  23662  cnprest2  23663  lmss  23671  haust1  23725  nrmsep3  23728  isnrm2  23731  lmmo  23753  fincmp  23766  cmpsublem  23772  cmpsub  23773  uncmp  23776  hauscmplem  23779  dfconn2  23792  iunconnlem  23800  unconn  23802  is1stc2  23815  1stcrest  23826  1stcelcls  23835  llyi  23848  nllyi  23849  subislly  23855  lly1stc  23870  txcnp  23994  txcnmpt  23998  hausdiag  24019  kqcldsat  24107  isfbas2  24209  isfil2  24230  fbasfip  24242  elfg  24245  filconn  24257  rnelfmlem  24326  rnelfm  24327  fmfnfmlem2  24329  fmfnfmlem4  24331  fmfnfm  24332  flimrest  24357  hauspwpwf1  24361  fclsrest  24398  alexsubALTlem2  24422  alexsubALTlem3  24423  alexsubALTlem4  24424  alexsubALT  24425  istmd  24448  istgp  24451  tsmssubm  24517  tsmssplit  24526  istrg  24538  istdrg  24540  istlm  24559  ustfilxp  24587  utoptop  24608  utop3cls  24625  bldisj  24772  blin  24795  blres  24805  lpbl  24877  metrest  24898  restmetu  24944  isngp  24970  isnlm  25049  isnmhm  25120  xrtgioo  25181  xrsmopn  25187  icccmplem2  25198  reconnlem2  25202  icoopnst  25315  iocopnst  25316  bndth  25334  zclmncvs  25524  isncvsngp  25525  ncvsprp  25528  ncvsm1  25530  ncvsdif  25531  ncvspi  25532  ncvs1  25533  ncvspds  25537  iscph  25546  tcphcph  25613  cfilfcls  25650  cmetcaulem  25664  isbn  25714  cldcss2  25818  hlhil  25819  ovolfcl  25842  ovolicc2lem2  25894  ovolicc2  25898  shftmbl  25914  volfiniun  25923  mbfmax  26025  mbfimaopnlem  26031  mbfaddlem  26036  i1faddlem  26069  i1fmullem  26070  i1fres  26081  itg1climres  26090  mbfi1fseqlem4  26094  itg2splitlem  26124  itg2split  26125  itgresr  26154  ellimc2  26252  ellimc3  26254  limcun  26270  dvreslem  26284  dvne0  26386  itgsubstlem  26423  ig1pval3  26551  aaliou2  26724  aaliou2b  26725  pilem1  26835  rlimcnp2  27351  fsumharmonic  27396  ppisval2  27489  prmorcht  27562  fsumvma2  27598  pclogsum  27599  vmasum  27600  chpchtsum  27603  chpub  27604  rpvmasum2  27896  madeval2  28276  tglineineq  29168  angmgmaddcpbl  29447  trlsegvdeg  30885  frgrncvvdeqlem7  30963  frgrncvvdeqlem9  30965  minvecolem1  31533  minvecolem4a  31536  minvecolem4b  31537  minvecolem4  31539  h2hcau  31638  axhcompl-zf  31657  hhcmpl  31859  hhcms  31862  ocin  31955  ocnel  31957  shmodsi  32048  pjhthlem2  32051  omlsilem  32061  pjoc1i  32090  spansnm0i  32309  nonbooli  32310  5oalem7  32319  3oalem3  32323  pjssmii  32340  mayete3i  32387  nmcopex  32688  nmcoplb  32689  lncnopbd  32696  nmcfnex  32712  nmcfnlb  32713  riesz4  32723  riesz1  32724  riesz2  32725  cnlnadjlem3  32728  cnlnadjlem5  32730  cnlnadjlem9  32734  cnlnadjeu  32737  rnbra  32766  pjimai  32835  pjclem4a  32857  pj3lem1  32865  jpi  32929  sumdmdii  33074  sumdmdlem  33077  sumdmdlem2  33078  cdjreui  33091  cdj3lem1  33093  iunin1f  33250  disjorf  33271  ofpreima  33357  1stpreima  33397  2ndpreima  33398  iocinioc2  33467  ssnnssfz  33475  cntzun  33739  kerunit  33990  ressply1mon1p  34203  ccfldextdgrr  34415  crefdf  34591  cmppcmp  34601  cnre2csqima  34654  ordtconnlem1  34667  lmxrge0  34695  isrrext  34743  esum0  34792  esumcst  34806  esumpcvgval  34821  esumcvg  34829  measvuni  34958  eulerpartlemt0  35112  eulerpartlemr  35117  eulerpartlemgf  35122  eulerpartlemgs2  35123  eulerpartlemn  35124  fiblem  35141  oddprm2  35395  bnj1173  35743  bnj1174  35744  bnj1279  35759  elima4  36755  dfon2lem4  36763  ellimits  36887  dfom5b  36889  brapply  36915  brcap  36917  dfrecs2  36929  dfrdg4  36930  finminlem  37321  neibastop2lem  37363  neibastop2  37364  neifg  37374  tailfb  37380  onsucconni  37440  onintopssconn  37443  onsucsuccmpi  37446  limsucncmpi  37448  onint1  37452  mh-infprim2bi  37550  bj-inex1gALT  38052  bj-inrab  38055  bj-rcleqf  38153  bj-inxpALT  38176  bj-elinxp  38177  bj-restuni  38288  bj-idres  38349  bj-opelidres  38350  bj-eldiag  38365  bj-eldiag2  38366  bj-ccinftydisj  38402  taupilem3  38508  isbasisrelowllem1  38546  isbasisrelowllem2  38547  nlpineqsn  38599  fvineqsneu  38602  ptrest  38805  poimirlem29  38835  poimirlem30  38836  mblfinlem2  38844  mbfposadd  38853  itg2gt0cn  38861  dvasin  38890  inixp  38930  0totbnd  38973  sstotbnd3  38976  heibor1lem  39009  heibor1  39010  heiborlem6  39016  isexid2  39055  smgrpismgmOLD  39062  issmgrpOLD  39063  mndoissmgrpOLD  39068  ismndo  39072  exidresid  39079  rngo1cl  39139  isfld2  39205  ineleq  39552  refressn  39731  eleccossin  39771  elrefsymrelsrel  39853  dfeldisj3  40009  eldisjdmqsim  40015  disjlem14  40099  prtlem14  40197  lshpdisj  40310  lkrin  40487  ishlat1  40675  pmodlem2  41170  pclfinN  41223  pclcmpatN  41224  osumcllem4N  41282  pexmidlem1N  41293  dihmeetlem1N  42613  dihglblem5apreN  42614  dihmeetlem4preN  42629  dihmeetlem13N  42642  dochnel2  42715  lcdlss  42942  mapd1o  42971  baerlem3lem2  43033  baerlem5alem2  43034  baerlem5blem2  43035  redvmptabs  43677  cmpfiiin  43974  mrefg2  43984  fz1eqin  44046  islmodfg  44337  islssfg2  44339  lnr2i  44383  rp-fakeinunass  44777  fiinfi  44835  elinintab  44837  elinintrab  44839  elinlem  44859  cnvcnvintabd  44861  ntrneikb  45355  ntrneik3  45357  ntrneik13  45359  ismnushort  45546  radcnvrat  45559  nzin  45563  onfrALTlem2  45789  onfrALTlem2VD  46131  relpmin  46206  pwclaxpow  46238  dfac5prim  46244  modelac8prim  46246  permac8prim  46268  iooabslt  46784  iccintsng  46808  lptioo2cn  46928  lptioo1cn  46929  cncfuni  47169  icccncfext  47170  stoweidlem44  47327  fourierdlem42  47432  fourierdlem80  47469  sge00  47659  wrddin2  48171  chndin2  48176  chnrin2  48181  eldmressn  48380  afvres  48515  afv2res  48582  prproropf1olem0  48857  31prm  48955  indprmfz  48988  rngccatidALTV  49642  rhmsubcALTVlem3  49653  funcringcsetcALTV2lem7  49666  ringccatidALTV  49676  ringcbasbasALTV  49682  funcringcsetclem7ALTV  49689  fldhmsubcALTV  49703  dfidom2  49771  ssnn0ssfz  49792  elbigo2  49995  itsclinecirc0in  50218  resinsnALT  50317  opndisj  50348  clddisj  50349  i0oii  50365  io1ii  50366