Theorem elin 3387

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

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1395   e. wcel 2200   _Vcvv 2799   i^i cin 3196

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-in 3203

This theorem is referenced by:  elini  3388  elind  3389  elinel1  3390  elinel2  3391  elin2  3392  elin3  3395  incom  3396  ineqri  3397  ineq1  3398  inass  3414  inss1  3424  ssin  3426  ssrin  3429  dfss4st  3437  inssdif  3440  difin  3441  unssin  3443  inssun  3444  invdif  3446  indif  3447  indi  3451  undi  3452  difundi  3456  difindiss  3458  indifdir  3460  difin2  3466  inrab2  3477  inelcm  3552  inssdif0im  3559  uniin  3908  intun  3954  intpr  3955  elrint  3963  iunin2  4029  iinin2m  4034  elriin  4036  disjnim  4073  disjiun  4078  brin  4136  trin  4192  inex1  4218  inuni  4239  bnd2  4257  ordpwsucss  4659  ordpwsucexmid  4662  peano5  4690  inopab  4854  inxp  4856  dmin  4931  opelres  5010  intasym  5113  asymref  5114  dminss  5143  imainss  5144  inimasn  5146  ssrnres  5171  cnvresima  5218  dfco2a  5229  funinsn  5370  imainlem  5402  imain  5403  2elresin  5434  nfvres  5665  respreima  5765  isoini  5948  offval  6232  tfrlem5  6466  mapval2  6833  ixpin  6878  ssenen  7020  infidc  7112  fnfi  7114  peano5nnnn  8090  peano5nni  9124  ixxdisj  10111  icodisj  10200  fzdisj  10260  uzdisj  10301  nn0disj  10346  fzouzdisj  10390  isumss  11918  fsumsplit  11934  sumsplitdc  11959  fsum2dlemstep  11961  fprod2dlemstep  12149  bitsmod  12483  bitsinv1  12489  4sqlem12  12941  nninfdclemcl  13035  nninfdclemp1  13037  insubm  13534  isrhm  14138  subsubrng2  14195  subsubrg2  14226  2idlelb  14485  isbasis2g  14735  tgval2  14741  tgcl  14754  epttop  14780  ssntr  14812  ntreq0  14822  cnptopresti  14928  cnptoprest  14929  cnptoprest2  14930  lmss  14936  txcnp  14961  txcnmpt  14963  bldisj  15091  blininf  15114  blres  15124  metrest  15196  pilem1  15469  wlk1walkdom  16105  bj-charfundcALT  16255  bj-charfunr  16256  bdinex1  16345  bj-indind  16378