Theorem elin 3392

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 2815	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 2815	. . 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 3207	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 2954	. 2 |- ( A e. _V -> ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) ) )
9	1, 3, 8	pm5.21nii 712	1 |- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1398   e. wcel 2202   _Vcvv 2803   i^i cin 3200

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-in 3207

This theorem is referenced by:  elini  3393  elind  3394  elinel1  3395  elinel2  3396  elin2  3397  elin3  3400  incom  3401  ineqri  3402  ineq1  3403  inass  3419  inss1  3429  ssin  3431  ssrin  3434  dfss4st  3442  inssdif  3445  difin  3446  unssin  3448  inssun  3449  invdif  3451  indif  3452  indi  3456  undi  3457  difundi  3461  difindiss  3463  indifdir  3465  difin2  3471  inrab2  3482  inelcm  3557  inssdif0im  3564  uniin  3918  intun  3964  intpr  3965  elrint  3973  iunin2  4039  iinin2m  4044  elriin  4046  disjnim  4083  disjiun  4088  brin  4146  trin  4202  inex1  4228  inuni  4250  bnd2  4269  ordpwsucss  4671  ordpwsucexmid  4674  peano5  4702  inopab  4868  inxp  4870  dmin  4945  opelres  5024  intasym  5128  asymref  5129  dminss  5158  imainss  5159  inimasn  5161  ssrnres  5186  cnvresima  5233  dfco2a  5244  funinsn  5386  imainlem  5418  imain  5419  2elresin  5450  nfvres  5684  respreima  5783  isoini  5969  offval  6252  tfrlem5  6523  mapval2  6890  ixpin  6935  ssenen  7080  infidc  7176  fnfi  7178  peano5nnnn  8172  peano5nni  9205  ixxdisj  10199  icodisj  10288  fzdisj  10349  uzdisj  10390  nn0disj  10435  fzouzdisj  10479  isumss  12032  fsumsplit  12048  sumsplitdc  12073  fsum2dlemstep  12075  fprod2dlemstep  12263  bitsmod  12597  bitsinv1  12603  4sqlem12  13055  nninfdclemcl  13149  nninfdclemp1  13151  insubm  13648  isrhm  14253  subsubrng2  14310  subsubrg2  14341  2idlelb  14601  isbasis2g  14856  tgval2  14862  tgcl  14875  epttop  14901  ssntr  14933  ntreq0  14943  cnptopresti  15049  cnptoprest  15050  cnptoprest2  15051  lmss  15057  txcnp  15082  txcnmpt  15084  bldisj  15212  blininf  15235  blres  15245  metrest  15317  pilem1  15590  wlk1walkdom  16300  trlsegvdegfi  16408  bj-charfundcALT  16525  bj-charfunr  16526  bdinex1  16615  bj-indind  16648