Theorem elin 3347

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 2774	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 2774	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 277	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2259	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2259	. . . 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 3163	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 2911	. 2 |- ( A e. _V -> ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) ) )
9	1, 3, 8	pm5.21nii 705	1 |- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1364   e. wcel 2167   _Vcvv 2763   i^i cin 3156

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-in 3163

This theorem is referenced by:  elini  3348  elind  3349  elinel1  3350  elinel2  3351  elin2  3352  elin3  3355  incom  3356  ineqri  3357  ineq1  3358  inass  3374  inss1  3384  ssin  3386  ssrin  3389  dfss4st  3397  inssdif  3400  difin  3401  unssin  3403  inssun  3404  invdif  3406  indif  3407  indi  3411  undi  3412  difundi  3416  difindiss  3418  indifdir  3420  difin2  3426  inrab2  3437  inelcm  3512  inssdif0im  3519  uniin  3860  intun  3906  intpr  3907  elrint  3915  iunin2  3981  iinin2m  3986  elriin  3988  disjnim  4025  disjiun  4029  brin  4086  trin  4142  inex1  4168  inuni  4189  bnd2  4207  ordpwsucss  4604  ordpwsucexmid  4607  peano5  4635  inopab  4799  inxp  4801  dmin  4875  opelres  4952  intasym  5055  asymref  5056  dminss  5085  imainss  5086  inimasn  5088  ssrnres  5113  cnvresima  5160  dfco2a  5171  funinsn  5308  imainlem  5340  imain  5341  2elresin  5370  nfvres  5593  respreima  5691  isoini  5866  offval  6145  tfrlem5  6374  mapval2  6739  ixpin  6784  ssenen  6914  infidc  7002  fnfi  7004  peano5nnnn  7962  peano5nni  8996  ixxdisj  9981  icodisj  10070  fzdisj  10130  uzdisj  10171  nn0disj  10216  fzouzdisj  10259  isumss  11559  fsumsplit  11575  sumsplitdc  11600  fsum2dlemstep  11602  fprod2dlemstep  11790  bitsmod  12124  bitsinv1  12130  4sqlem12  12582  nninfdclemcl  12676  nninfdclemp1  12678  insubm  13143  isrhm  13740  subsubrng2  13797  subsubrg2  13828  2idlelb  14087  isbasis2g  14307  tgval2  14313  tgcl  14326  epttop  14352  ssntr  14384  ntreq0  14394  cnptopresti  14500  cnptoprest  14501  cnptoprest2  14502  lmss  14508  txcnp  14533  txcnmpt  14535  bldisj  14663  blininf  14686  blres  14696  metrest  14768  pilem1  15041  bj-charfundcALT  15481  bj-charfunr  15482  bdinex1  15571  bj-indind  15604