Theorem elin 2197

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 1808	. 2 |- (A e. (B i^i C) -> A e. V)
2		elisset 1808	. . 3 |- (A e. C -> A e. V)
3	2	adantl 388	. 2 |- ((A e. B /\ A e. C) -> A e. V)
4		eleq1 1526	. . . 4 |- (x = A -> (x e. B <-> A e. B))
5		eleq1 1526	. . . 4 |- (x = A -> (x e. C <-> A e. C))
6	4, 5	anbi12d 626	. . 3 |- (x = A -> ((x e. B /\ x e. C) <-> (A e. B /\ A e. C)))
7		df-in 2041	. . 3 |- (B i^i C) = {x | (x e. B /\ x e. C)}
8	6, 7	elab2g 1891	. 2 |- (A e. V -> (A e. (B i^i C) <-> (A e. B /\ A e. C)))
9	1, 3, 8	pm5.21nii 677	1 |- (A e. (B i^i C) <-> (A e. B /\ A e. C))

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  Vcvv 1802   i^i cin 2036

This theorem is referenced by:  incom 2198  ineqri 2199  ineq1 2200  hbin 2210  rabbirdv 2211  inass 2213  inss1 2220  ssrin 2224  dfss4 2232  dfin2 2234  difin 2235  indi 2241  undi 2242  unineq 2245  inab 2258  inrab2 2262  inelcm 2313  difin0ss 2322  inssdif0 2323  disjsn 2431  uniin 2510  intun 2552  intpr 2553  iunin2 2598  trin 2680  inex1 2706  frirr 2914  wefrc 2933  ordtri3or 2969  ordpwsuc 3056  brinxp2 3221  inopab 3258  inxp 3259  dmin 3307  opelres 3356  dfima2 3389  intasym 3422  asymref 3423  asymrefOLD 3425  intirr 3427  cnvin 3442  dminss 3448  imainss 3449  ssrnres 3467  funin 3552  2elresin 3584  nfvres 3733  funfvima 3837  isomin 3884  isoini 3885  tfrlem5 3900  tz7.48-2 3942  mapval2 4319  pw2en 4426  sbthcl 4439  ssenen 4484  inf3lem2 4586  zfregs 4619  cp 4694  bnd2 4696  aceq5lem1 4707  aceq5lem5 4711  aceq5 4712  kmlem3 4739  kmlem14 4750  kmlem15 4751  ltpiord 4987  ltxrt 5467  clm4 7018  isbasis2g 7554  tgval2t 7559  tgclt 7566  tgss3t 7580  basgent 7582  opnin 7809  lmss 7888  isphg 8407  ishl 8522  axgroth4 8719  grothprim 8722  hhcmpl 8990  ocin 9085  ocnelt 9086  chocuni 9088  omlsilem 9159  pjoc1 9179  shmods 9277  spansnm0 9512  nonbool 9513  5oalem1 9516  5oalem2 9517  5oalem4 9519  5oalem5 9520  5oalem7 9522  3oalem2 9525  3oalem3 9526  pjssm 9543  mayete3 9590  nmcopext 9874  nmcoplbt 9875  lncnopbd 9881  nmcfnext 9903  nmcfnlbt 9904  riesz4t 9912  riesz1t 9913  riesz2t 9914  cnlnadjlem3 9917  cnlnadjlem4 9918  cnlnadjlem5 9919  cnlnadjlem9 9923  cnlnadjeut 9926  rnbra 9953  pjima 10015  dfpjopt 10021  pjclem4a 10036  pjclem4 10037  pj3lem1 10044  pj3s 10045  jp 10107  sumdmdi 10249  sumdmdlem 10252  sumdmdlem2 10253  cdjreu 10264  cdj3lem1 10266  ntunte 10340  uninqs 10342  filintf 10443

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-in 2041

Copyright terms: Public domain