Theorem elin 2210

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 1820	. 2 |- (A e. (B i^i C) -> A e. V)
2		elisset 1820	. . 3 |- (A e. C -> A e. V)
3	2	adantl 390	. 2 |- ((A e. B /\ A e. C) -> A e. V)
4		eleq1 1537	. . . 4 |- (x = A -> (x e. B <-> A e. B))
5		eleq1 1537	. . . 4 |- (x = A -> (x e. C <-> A e. C))
6	4, 5	anbi12d 630	. . 3 |- (x = A -> ((x e. B /\ x e. C) <-> (A e. B /\ A e. C)))
7		df-in 2054	. . 3 |- (B i^i C) = {x | (x e. B /\ x e. C)}
8	6, 7	elab2g 1903	. 2 |- (A e. V -> (A e. (B i^i C) <-> (A e. B /\ A e. C)))
9	1, 3, 8	pm5.21nii 681	1 |- (A e. (B i^i C) <-> (A e. B /\ A e. C))

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 958   e. wcel 960  Vcvv 1814   i^i cin 2049

This theorem is referenced by:  incom 2211  ineqri 2212  ineq1 2213  hbin 2223  rabbirdv 2224  inass 2226  inss1 2233  ssrin 2237  dfss4 2245  dfin2 2247  difin 2248  indi 2254  undi 2255  unineq 2258  inab 2271  inrab2 2275  inelcm 2327  difin0ss 2336  inssdif0 2337  disjsn 2445  uniin 2524  intun 2566  intpr 2567  iunin2 2613  trin 2695  inex1 2721  frirr 2930  wefrc 2949  ordtri3or 2985  ordpwsuc 3072  brinxp2 3237  inopab 3274  inxp 3275  dmin 3324  opelres 3378  dfima2 3411  intasym 3444  asymref 3445  intirr 3447  cnvin 3462  dminss 3468  imainss 3469  ssrnres 3487  funin 3572  2elresin 3604  nfvres 3754  funfvima 3858  isomin 3905  isoini 3906  tfrlem5 3921  tz7.48-2 3963  mapval2 4341  pw2en 4452  sbthcl 4465  ssenen 4510  inf3lem2 4623  zfregs 4657  cp 4732  bnd2 4734  aceq5lem1 4745  aceq5lem5 4749  aceq5 4750  kmlem3 4777  kmlem14 4788  kmlem15 4789  ltpiord 5027  ltxrt 5507  clm4 7080  infpss 7575  isbasis2g 7611  tgval2t 7616  tgclt 7623  tgss3t 7637  basgent 7639  opnin 7866  lmss 7950  isphg 8472  ishl 8587  axgroth4 8775  grothprim 8778  axhcompl 8863  hhcmpl 9064  ocin 9164  ocnelt 9165  chocuni 9167  projlemHIL 9213  omlsilem 9239  pjoc1 9259  shmods 9357  spansnm0 9590  nonbool 9591  5oalem1 9594  5oalem2 9595  5oalem4 9597  5oalem5 9598  5oalem7 9600  3oalem2 9603  3oalem3 9604  pjssm 9621  mayete3 9668  nmcopext 9954  nmcoplbt 9955  lncnopbd 9961  nmcfnext 9983  nmcfnlbt 9984  riesz4t 9992  riesz1t 9993  riesz2t 9994  cnlnadjlem3 9997  cnlnadjlem4 9998  cnlnadjlem5 9999  cnlnadjlem9 10003  cnlnadjeut 10006  rnbra 10035  pjima 10099  dfpjopt 10106  pjclem4a 10121  pjclem4 10122  pj3lem1 10129  pj3s 10130  jp 10192  sumdmdi 10337  sumdmdlem 10340  sumdmdlem2 10341  cdjreu 10354  cdj3lem1 10356  ntunte 10434  uninqs 10436  inposet 10477  filintf 10554  sfvlim 10576

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-in 2054

Copyright terms: Public domain