Theorem elin 1635

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 1354	. 2 |- (A e. (B i^i C) -> A e. V)
2		elisset 1354	. . 3 |- (A e. C -> A e. V)
3	2	adantl 305	. 2 |- ((A e. B /\ A e. C) -> A e. V)
4		eleq1 1149	. . . 4 |- (x = A -> (x e. B <-> A e. B))
5		eleq1 1149	. . . 4 |- (x = A -> (x e. C <-> A e. C))
6	4, 5	anbi12d 476	. . 3 |- (x = A -> ((x e. B /\ x e. C) <-> (A e. B /\ A e. C)))
7		df-in 1491	. . 3 |- (B i^i C) = {x | (x e. B /\ x e. C)}
8	6, 7	elab2g 1418	. 2 |- (A e. V -> (A e. (B i^i C) <-> (A e. B /\ A e. C)))
9	1, 3, 8	pm5.21nii 504	1 |- (A e. (B i^i C) <-> (A e. B /\ A e. C))

Syntax hints:   <-> wb 127   /\ wa 196   = wceq 1091   e. wcel 1092  Vcvv 1348   i^i cin 1486

This theorem is referenced by:  incom 1636  ineqri 1637  ineq1 1638  hbin 1647  birabrdv 1648  inass 1650  inss1 1657  ssrin 1661  dfss4 1667  dfin2 1669  difin 1670  indi 1676  undi 1677  unineq 1680  inab 1692  inex1 1697  inelcm 1742  difin0ss 1753  inssdif0 1754  disjsn 1836  uniin 1935  intun 1989  intpr 1990  iunin2 2030  trin 2051  frirr 2176  wefrc 2195  ordtri3or 2230  onpwsuc 2315  brinxp 2466  inopab 2495  inxp 2496  dmin 2537  opelres 2579  dfima2 2604  intasym 2627  intirr 2628  cnvin 2643  dminss 2648  imainss 2649  funin 2708  2elresin 2733  nfvres 2850  funfvima 2904  isomin 2937  isoini 2938  tfrlem5 2953  tz7.48-2 2995  pw2en 3348  sbthcl 3361  ssenen 3399  inf3lem2 3465  zfregs 3491  cp 3547  bnd2 3549  aceq5lem1 3558  aceq5lem5 3562  aceq5 3563  kmlem3 3582  kmlem14 3593  kmlem15 3594  ltpiord 3809  ocin 5177  chocuni 5179  omlsilem 5249  pjoc1 5268  pjoml 5271  shmods 5363  5oalem1 5544  5oalem2 5545  5oalem4 5547  5oalem5 5548  5oalem7 5550  3oalem2 5553  3oalem3 5554  pjssm 5572  pjclem4a 5652  pjclem4 5653  pj3lem1 5658  pj3s 5659  jp 5703  sumdmdi 5785  sumdmdlem 5786  sumdmd 5787

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-in 1491

metamath.org