Theorem elin 3310

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 2741	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 2741	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 275	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2233	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2233	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
6	4, 5	anbi12d 470	. . 3 |- ( x = A -> ( ( x e. B /\ x e. C ) <-> ( A e. B /\ A e. C ) ) )
7		df-in 3127	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 2877	. 2 |- ( A e. _V -> ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) ) )
9	1, 3, 8	pm5.21nii 699	1 |- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )

Syntax hints:   /\ wa 103   <-> wb 104   = wceq 1348   e. wcel 2141   _Vcvv 2730   i^i cin 3120

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127

This theorem is referenced by:  elini  3311  elind  3312  elinel1  3313  elinel2  3314  elin2  3315  elin3  3318  incom  3319  ineqri  3320  ineq1  3321  inass  3337  inss1  3347  ssin  3349  ssrin  3352  dfss4st  3360  inssdif  3363  difin  3364  unssin  3366  inssun  3367  invdif  3369  indif  3370  indi  3374  undi  3375  difundi  3379  difindiss  3381  indifdir  3383  difin2  3389  inrab2  3400  inelcm  3474  inssdif0im  3481  uniin  3814  intun  3860  intpr  3861  elrint  3869  iunin2  3934  iinin2m  3939  elriin  3941  disjnim  3978  disjiun  3982  brin  4039  trin  4095  inex1  4121  inuni  4139  bnd2  4157  ordpwsucss  4549  ordpwsucexmid  4552  peano5  4580  inopab  4741  inxp  4743  dmin  4817  opelres  4894  intasym  4993  asymref  4994  dminss  5023  imainss  5024  inimasn  5026  ssrnres  5051  cnvresima  5098  dfco2a  5109  funinsn  5245  imainlem  5277  imain  5278  2elresin  5307  nfvres  5527  respreima  5621  isoini  5794  offval  6065  tfrlem5  6290  mapval2  6652  ixpin  6697  ssenen  6825  fnfi  6910  peano5nnnn  7841  peano5nni  8868  ixxdisj  9847  icodisj  9936  fzdisj  9995  uzdisj  10036  nn0disj  10081  fzouzdisj  10123  isumss  11341  fsumsplit  11357  sumsplitdc  11382  fsum2dlemstep  11384  fprod2dlemstep  11572  nninfdclemcl  12390  nninfdclemp1  12392  insubm  12690  isbasis2g  12796  tgval2  12804  tgcl  12817  epttop  12843  ssntr  12875  ntreq0  12885  cnptopresti  12991  cnptoprest  12992  cnptoprest2  12993  lmss  12999  txcnp  13024  txcnmpt  13026  bldisj  13154  blininf  13177  blres  13187  metrest  13259  pilem1  13453  bj-charfundcALT  13804  bj-charfunr  13805  bdinex1  13894  bj-indind  13927