Theorem elin 3404

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 2827	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 2827	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 277	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2297	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2297	. . . 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 3219	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 2966	. 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 2205   _Vcvv 2815   i^i cin 3212

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 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-in 3219

This theorem is referenced by:  elini  3405  elind  3406  elinel1  3407  elinel2  3408  elin2  3409  elin3  3412  incom  3413  ineqri  3416  ineq1  3417  inass  3433  inss1  3443  ssin  3445  ssrin  3448  dfss4st  3456  inssdif  3459  difin  3460  unssin  3462  inssun  3463  invdif  3465  indif  3466  indi  3470  undi  3471  difundi  3475  difindiss  3477  indifdir  3479  difin2  3485  inrab2  3496  inelcm  3571  inssdif0im  3578  uniin  3936  intun  3982  intpr  3983  elrint  3991  iunin2  4057  iinin2m  4062  elriin  4064  disjnim  4101  disjiun  4106  brin  4164  trin  4220  inex1  4246  inuni  4269  bnd2  4288  ordpwsucss  4691  ordpwsucexmid  4694  peano5  4722  inopab  4889  inxp  4891  dmin  4966  opelres  5045  intasym  5149  asymref  5150  dminss  5179  imainss  5180  inimasn  5182  ssrnres  5207  cnvresima  5254  dfco2a  5265  funinsn  5407  imainlem  5439  imain  5440  2elresin  5471  nfvres  5708  respreima  5807  isoini  5993  offval  6276  tfrlem5  6547  mapval2  6914  ixpin  6960  ssenen  7107  infidc  7203  fnfi  7205  elfpw  7217  peano5nnnn  8209  peano5nni  9242  ixxdisj  10239  icodisj  10328  fzdisj  10389  uzdisj  10431  nn0disj  10476  fzouzdisj  10520  sseqn  11207  hashfibclem  11210  isumss  12081  fsumsplit  12097  sumsplitdc  12122  fsum2dlemstep  12124  fprod2dlemstep  12312  bitsmod  12646  bitsinv1  12652  4sqlem12  13104  ballotfilem2  13149  nninfdclemcl  13216  nninfdclemp1  13218  insubm  13715  isrhm  14320  subsubrng2  14377  subsubrg2  14408  2idlelb  14670  isbasis2g  14927  tgval2  14933  tgcl  14946  epttop  14972  ssntr  15004  ntreq0  15014  cnptopresti  15120  cnptoprest  15121  cnptoprest2  15122  lmss  15128  txcnp  15153  txcnmpt  15155  bldisj  15283  blininf  15306  blres  15316  metrest  15388  pilem1  15661  wlk1walkdom  16371  trlsegvdegfi  16479  bj-charfundcALT  16596  bj-charfunr  16597  bdinex1  16686  bj-indind  16719