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  5663  respreima  5763  isoini  5942  offval  6226  tfrlem5  6460  mapval2  6825  ixpin  6870  ssenen  7012  infidc  7101  fnfi  7103  peano5nnnn  8079  peano5nni  9113  ixxdisj  10099  icodisj  10188  fzdisj  10248  uzdisj  10289  nn0disj  10334  fzouzdisj  10378  isumss  11902  fsumsplit  11918  sumsplitdc  11943  fsum2dlemstep  11945  fprod2dlemstep  12133  bitsmod  12467  bitsinv1  12473  4sqlem12  12925  nninfdclemcl  13019  nninfdclemp1  13021  insubm  13518  isrhm  14122  subsubrng2  14179  subsubrg2  14210  2idlelb  14469  isbasis2g  14719  tgval2  14725  tgcl  14738  epttop  14764  ssntr  14796  ntreq0  14806  cnptopresti  14912  cnptoprest  14913  cnptoprest2  14914  lmss  14920  txcnp  14945  txcnmpt  14947  bldisj  15075  blininf  15098  blres  15108  metrest  15180  pilem1  15453  wlk1walkdom  16070  bj-charfundcALT  16172  bj-charfunr  16173  bdinex1  16262  bj-indind  16295