Theorem elin 3300

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 2732	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 2732	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 275	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2227	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2227	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
6	4, 5	anbi12d 465	. . 3 |- ( x = A -> ( ( x e. B /\ x e. C ) <-> ( A e. B /\ A e. C ) ) )
7		df-in 3117	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 2868	. 2 |- ( A e. _V -> ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) ) )
9	1, 3, 8	pm5.21nii 694	1 |- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )

Syntax hints:   /\ wa 103   <-> wb 104   = wceq 1342   e. wcel 2135   _Vcvv 2721   i^i cin 3110

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 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723  df-in 3117

This theorem is referenced by:  elini  3301  elind  3302  elinel1  3303  elinel2  3304  elin2  3305  elin3  3308  incom  3309  ineqri  3310  ineq1  3311  inass  3327  inss1  3337  ssin  3339  ssrin  3342  dfss4st  3350  inssdif  3353  difin  3354  unssin  3356  inssun  3357  invdif  3359  indif  3360  indi  3364  undi  3365  difundi  3369  difindiss  3371  indifdir  3373  difin2  3379  inrab2  3390  inelcm  3464  inssdif0im  3471  uniin  3803  intun  3849  intpr  3850  elrint  3858  iunin2  3923  iinin2m  3928  elriin  3930  disjnim  3967  disjiun  3971  brin  4028  trin  4084  inex1  4110  inuni  4128  bnd2  4146  ordpwsucss  4538  ordpwsucexmid  4541  peano5  4569  inopab  4730  inxp  4732  dmin  4806  opelres  4883  intasym  4982  asymref  4983  dminss  5012  imainss  5013  inimasn  5015  ssrnres  5040  cnvresima  5087  dfco2a  5098  funinsn  5231  imainlem  5263  imain  5264  2elresin  5293  nfvres  5513  respreima  5607  isoini  5780  offval  6051  tfrlem5  6273  mapval2  6635  ixpin  6680  ssenen  6808  fnfi  6893  peano5nnnn  7824  peano5nni  8851  ixxdisj  9830  icodisj  9919  fzdisj  9977  uzdisj  10018  nn0disj  10063  fzouzdisj  10105  isumss  11318  fsumsplit  11334  sumsplitdc  11359  fsum2dlemstep  11361  fprod2dlemstep  11549  nninfdclemcl  12320  nninfdclemp1  12322  isbasis2g  12584  tgval2  12592  tgcl  12605  epttop  12631  ssntr  12663  ntreq0  12673  cnptopresti  12779  cnptoprest  12780  cnptoprest2  12781  lmss  12787  txcnp  12812  txcnmpt  12814  bldisj  12942  blininf  12965  blres  12975  metrest  13047  pilem1  13241  bj-charfundcALT  13526  bj-charfunr  13527  bdinex1  13616  bj-indind  13649