Theorem elin 3356

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

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1373   e. wcel 2176   _Vcvv 2772   i^i cin 3165

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-in 3172

This theorem is referenced by:  elini  3357  elind  3358  elinel1  3359  elinel2  3360  elin2  3361  elin3  3364  incom  3365  ineqri  3366  ineq1  3367  inass  3383  inss1  3393  ssin  3395  ssrin  3398  dfss4st  3406  inssdif  3409  difin  3410  unssin  3412  inssun  3413  invdif  3415  indif  3416  indi  3420  undi  3421  difundi  3425  difindiss  3427  indifdir  3429  difin2  3435  inrab2  3446  inelcm  3521  inssdif0im  3528  uniin  3870  intun  3916  intpr  3917  elrint  3925  iunin2  3991  iinin2m  3996  elriin  3998  disjnim  4035  disjiun  4040  brin  4097  trin  4153  inex1  4179  inuni  4200  bnd2  4218  ordpwsucss  4616  ordpwsucexmid  4619  peano5  4647  inopab  4811  inxp  4813  dmin  4887  opelres  4965  intasym  5068  asymref  5069  dminss  5098  imainss  5099  inimasn  5101  ssrnres  5126  cnvresima  5173  dfco2a  5184  funinsn  5324  imainlem  5356  imain  5357  2elresin  5388  nfvres  5612  respreima  5710  isoini  5889  offval  6168  tfrlem5  6402  mapval2  6767  ixpin  6812  ssenen  6950  infidc  7038  fnfi  7040  peano5nnnn  8007  peano5nni  9041  ixxdisj  10027  icodisj  10116  fzdisj  10176  uzdisj  10217  nn0disj  10262  fzouzdisj  10306  isumss  11735  fsumsplit  11751  sumsplitdc  11776  fsum2dlemstep  11778  fprod2dlemstep  11966  bitsmod  12300  bitsinv1  12306  4sqlem12  12758  nninfdclemcl  12852  nninfdclemp1  12854  insubm  13350  isrhm  13953  subsubrng2  14010  subsubrg2  14041  2idlelb  14300  isbasis2g  14550  tgval2  14556  tgcl  14569  epttop  14595  ssntr  14627  ntreq0  14637  cnptopresti  14743  cnptoprest  14744  cnptoprest2  14745  lmss  14751  txcnp  14776  txcnmpt  14778  bldisj  14906  blininf  14929  blres  14939  metrest  15011  pilem1  15284  bj-charfundcALT  15782  bj-charfunr  15783  bdinex1  15872  bj-indind  15905