Theorem elin 2786

Description: Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25.

Assertion

Ref	Expression
elin	|- (A e. (B i^i C) <-> (A e. B /\ A e. C))

Proof of Theorem elin

Step	Hyp	Ref	Expression
1		elisset 2299	. 2 |- (A e. (B i^i C) -> A e. _V)
2		elisset 2299	. . 3 |- (A e. C -> A e. _V)
3	2	adantl 424	. 2 |- ((A e. B /\ A e. C) -> A e. _V)
4		eleq1 1957	. . . 4 |- (x = A -> (x e. B <-> A e. B))
5		eleq1 1957	. . . 4 |- (x = A -> (x e. C <-> A e. C))
6	4, 5	anbi12d 690	. . 3 |- (x = A -> ((x e. B /\ x e. C) <-> (A e. B /\ A e. C)))
7		df-in 2603	. . 3 |- (B i^i C) = {x | (x e. B /\ x e. C)}
8	6, 7	elab2g 2406	. 2 |- (A e. _V -> (A e. (B i^i C) <-> (A e. B /\ A e. C)))
9	1, 3, 8	pm5.21nii 743	1 |- (A e. (B i^i C) <-> (A e. B /\ A e. C))

Syntax hints:   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  _Vcvv 2292   i^i cin 2592

This theorem is referenced by:  incom 2787  ineqri 2788  ineq1 2789  hbin 2800  rabbirdvOLD 2802  inass 2804  inss1 2812  ssin 2814  ssrin 2817  ssrinOLD 2818  dfss4 2827  dfss4OLD 2828  dfin2 2830  difin 2831  difinOLD 2832  indi 2838  indiOLD 2839  undi 2840  undiOLD 2841  unineq 2844  inabOLD 2862  inrab2 2867  inelcm 2928  difin0ss 2939  inssdif0 2940  inssdif0OLD 2941  inundif 2951  disjsnOLD 3090  uniin 3197  uniinOLD 3198  intun 3249  intpr 3250  iunin2 3320  iinxprg 3326  brin 3388  trin 3422  inex1 3452  inuni 3470  frirr 3634  wefrc 3652  ordtri3or 3691  ordtri3orOLD 3692  ordpwsuc 3896  brinxp2 4057  inopab 4108  inxp 4109  inxpOLD 4110  dmin 4165  opelres 4222  dfima2OLD 4266  intasym 4306  intasymOLD 4307  asymref 4308  asymrefOLD 4309  intirrOLD 4313  cnvin 4324  dminss 4330  imainss 4331  ssrnres 4354  dfco2a 4394  dfco2aOLD 4395  funinOLD 4485  2elresin 4524  nfvres 4705  funfvima 4828  isomin 4876  isoini 4877  tfrlem5 5123  tz7.48-2 5166  mapval2 5394  pw2en 5505  sbthcl 5522  ssenen 5598  inf3lem2 5720  zfregs 5754  cp 5852  bnd2 5854  aceq5lem1 5897  aceq5lem5 5901  aceq5 5902  kmlem3 5929  kmlem14 5940  kmlem15 5941  ltpiord 6167  ltxr 6664  clm4i 8340  infpss 8843  isbasis2g 8881  tgval2 8887  tgcl 8894  tgss3 8908  basgen 8910  opnin 9146  lmss 9231  isphg 9817  ishl 9936  axgroth4 10139  grothprim 10141  fipreima 10175  istoset 10209  uptx 10226  subtopmetlem 10255  subtopmet 10256  isfbas2 10263  filintf 10274  elfg 10284  sfvlim 10296  cncomp 10331  fintopcomp 10333  usinuniop 10341  isexid2 10372  smgrpismgm 10379  smgrpisass 10380  issmgrp 10381  mndissmgrp 10386  mndisexid 10387  mndmgmid 10389  ismnd 10390  ismnd2 10392  ring1cl 10415  axhcompl 10500  hhcmpl 10702  ocin 10802  ocnel 10803  chocunii 10805  projlemHIL 10851  omlsilem 10877  pjoc1i 10897  shmodsi 10995  spansnm0i 11230  nonbooli 11231  5oalem1 11234  5oalem2 11235  5oalem4 11237  5oalem5 11238  5oalem7 11240  3oalem2 11243  3oalem3 11244  pjssmii 11261  mayete3i 11308  mayete3OLDi 11309  nmcopex 11596  nmcoplb 11597  lncnopbd 11603  nmcfnex 11625  nmcfnlb 11626  riesz4 11634  riesz1 11635  riesz2 11636  cnlnadjlem3 11639  cnlnadjlem4 11640  cnlnadjlem5 11641  cnlnadjlem9 11645  cnlnadjeu 11648  rnbra 11678  pjimai 11748  dfpjop 11755  pjclem4a 11771  pjclem4 11772  pj3lem1 11779  pj3si 11780  jpi 11842  sumdmdii 11987  sumdmdlem 11990  sumdmdlem2 11991  cdjreui 12004  cdj3lem1 12006  bnj521 12522  bnj1153 12946  bnj1164 12956  bnj1269 13027  bnj1380 13097  bnj1172 13440  bnj1173 13441  indifdi 13823  ressn0 13829  dfon2lem4 13852  elpred 13888  elpredg 13889  predel 13894  wfrlem5 13961  axfelem12 14042  axfelem15 14045  ellimits 14079  dfoprab4spop 14339  uninqs 14340  omslim 14420  inposet 14620  pospos 14635  tostos 14637  isdir2 14640  ablcomgrp 14702  expus 14726  symgfo 14730  fprodsub 14742  isfld 14775  fldi 14776  zrfld 14784  zintdom 14787  unint2t 14866  intcont 14914  sinempcomp 14953  indcomp 14955  topunfincomp 14957  stfincomp 14959  bwt2 14960  vtarsuelt 15272  partarelt2 15274  eltintpar 15276  inttaror 15277  inttarcar 15278  carinttar 15279  cardtar 15281  cartarlim 15282  elcarelcl 15283  isplibg 15319  cnvresima 15359  ioodisj 15364  finminlem 15367  subntr 15425  compsublem 15430  compsub 15431  cptclsscpt 15432  uncomp 15433  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem2 15438  alexsublem3 15439  alexsublem4 15440  alexsub 15441  dfcon2 15442  cnconn 15444  reconnlem1 15446  reconnlem3 15448  reconnlem4 15449  reconnlem5 15450  is1stc3 15469  isfne2 15481  lfinpfin 15513  comppfsc 15517  neifg 15559  ufprim 15569  filssufillem 15570  filcon 15580  rnelfmlem 15592  rnelfm 15593  fmfnfmlem2 15595  fmfnfmlem4 15597  fmfnfm 15598  tailfb 15639  difin2 15676  inpreima 15682  respreima 15684  inixp 15722  fipreimaOLD 15756  fzdisj 15793  blssp 15844  icoopnst 15876  iocopnst 15877  cnresima 15891  sstotbnd 15936  totbndss 15937  heiborlem1 15955  heiborlem10 15964  heiborlem11 15965  heiborlem13 15967  heiborlem18 15972  heiborlem21 15975  heiborlem23 15977  heiborlem32 15986  heiborlem38 15992  heiborlem41 15995  exidresid 16032  iscring 16145  fldcrng 16152  isfld2 16153  isdmn 16202  prtlem14 16277  smores 16446  isolat 16939  ishlat 17018  issdrng 17179  pmodlem1 17307  pmodlem2 17308  osumcllem4 17367  pexmidlem1 17378

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-in 2603

Copyright terms: Public domain