Theorem elin 3333

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

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1364   e. wcel 2160   _Vcvv 2752   i^i cin 3143

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-in 3150

This theorem is referenced by:  elini  3334  elind  3335  elinel1  3336  elinel2  3337  elin2  3338  elin3  3341  incom  3342  ineqri  3343  ineq1  3344  inass  3360  inss1  3370  ssin  3372  ssrin  3375  dfss4st  3383  inssdif  3386  difin  3387  unssin  3389  inssun  3390  invdif  3392  indif  3393  indi  3397  undi  3398  difundi  3402  difindiss  3404  indifdir  3406  difin2  3412  inrab2  3423  inelcm  3498  inssdif0im  3505  uniin  3844  intun  3890  intpr  3891  elrint  3899  iunin2  3965  iinin2m  3970  elriin  3972  disjnim  4009  disjiun  4013  brin  4070  trin  4126  inex1  4152  inuni  4170  bnd2  4188  ordpwsucss  4581  ordpwsucexmid  4584  peano5  4612  inopab  4774  inxp  4776  dmin  4850  opelres  4927  intasym  5028  asymref  5029  dminss  5058  imainss  5059  inimasn  5061  ssrnres  5086  cnvresima  5133  dfco2a  5144  funinsn  5281  imainlem  5313  imain  5314  2elresin  5343  nfvres  5564  respreima  5661  isoini  5836  offval  6109  tfrlem5  6334  mapval2  6699  ixpin  6744  ssenen  6874  infidc  6959  fnfi  6961  peano5nnnn  7916  peano5nni  8947  ixxdisj  9928  icodisj  10017  fzdisj  10077  uzdisj  10118  nn0disj  10163  fzouzdisj  10205  isumss  11426  fsumsplit  11442  sumsplitdc  11467  fsum2dlemstep  11469  fprod2dlemstep  11657  4sqlem12  12429  nninfdclemcl  12494  nninfdclemp1  12496  insubm  12930  isrhm  13501  subsubrng2  13555  subsubrg2  13586  2idlelb  13813  isbasis2g  13982  tgval2  13988  tgcl  14001  epttop  14027  ssntr  14059  ntreq0  14069  cnptopresti  14175  cnptoprest  14176  cnptoprest2  14177  lmss  14183  txcnp  14208  txcnmpt  14210  bldisj  14338  blininf  14361  blres  14371  metrest  14443  pilem1  14637  bj-charfundcALT  14999  bj-charfunr  15000  bdinex1  15089  bj-indind  15122