Theorem elin 3390

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	|- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )

Proof of Theorem elin

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2814	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 2814	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 277	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2294	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2294	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
6	4, 5	anbi12d 473	. . 3 |- ( x = A -> ( ( x e. B /\ x e. C ) <-> ( A e. B /\ A e. C ) ) )
7		df-in 3206	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 2953	. 2 |- ( A e. _V -> ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) ) )
9	1, 3, 8	pm5.21nii 711	1 |- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1397   e. wcel 2202   _Vcvv 2802   i^i cin 3199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-in 3206

This theorem is referenced by:  elini  3391  elind  3392  elinel1  3393  elinel2  3394  elin2  3395  elin3  3398  incom  3399  ineqri  3400  ineq1  3401  inass  3417  inss1  3427  ssin  3429  ssrin  3432  dfss4st  3440  inssdif  3443  difin  3444  unssin  3446  inssun  3447  invdif  3449  indif  3450  indi  3454  undi  3455  difundi  3459  difindiss  3461  indifdir  3463  difin2  3469  inrab2  3480  inelcm  3555  inssdif0im  3562  uniin  3913  intun  3959  intpr  3960  elrint  3968  iunin2  4034  iinin2m  4039  elriin  4041  disjnim  4078  disjiun  4083  brin  4141  trin  4197  inex1  4223  inuni  4245  bnd2  4263  ordpwsucss  4665  ordpwsucexmid  4668  peano5  4696  inopab  4862  inxp  4864  dmin  4939  opelres  5018  intasym  5121  asymref  5122  dminss  5151  imainss  5152  inimasn  5154  ssrnres  5179  cnvresima  5226  dfco2a  5237  funinsn  5379  imainlem  5411  imain  5412  2elresin  5443  nfvres  5675  respreima  5775  isoini  5959  offval  6243  tfrlem5  6480  mapval2  6847  ixpin  6892  ssenen  7037  infidc  7133  fnfi  7135  peano5nnnn  8112  peano5nni  9146  ixxdisj  10138  icodisj  10227  fzdisj  10287  uzdisj  10328  nn0disj  10373  fzouzdisj  10417  isumss  11970  fsumsplit  11986  sumsplitdc  12011  fsum2dlemstep  12013  fprod2dlemstep  12201  bitsmod  12535  bitsinv1  12541  4sqlem12  12993  nninfdclemcl  13087  nninfdclemp1  13089  insubm  13586  isrhm  14191  subsubrng2  14248  subsubrg2  14279  2idlelb  14538  isbasis2g  14788  tgval2  14794  tgcl  14807  epttop  14833  ssntr  14865  ntreq0  14875  cnptopresti  14981  cnptoprest  14982  cnptoprest2  14983  lmss  14989  txcnp  15014  txcnmpt  15016  bldisj  15144  blininf  15167  blres  15177  metrest  15249  pilem1  15522  wlk1walkdom  16229  trlsegvdegfi  16337  bj-charfundcALT  16455  bj-charfunr  16456  bdinex1  16545  bj-indind  16578