Theorem elin 3318

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

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1353   e. wcel 2148   _Vcvv 2737   i^i cin 3128

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-in 3135

This theorem is referenced by:  elini  3319  elind  3320  elinel1  3321  elinel2  3322  elin2  3323  elin3  3326  incom  3327  ineqri  3328  ineq1  3329  inass  3345  inss1  3355  ssin  3357  ssrin  3360  dfss4st  3368  inssdif  3371  difin  3372  unssin  3374  inssun  3375  invdif  3377  indif  3378  indi  3382  undi  3383  difundi  3387  difindiss  3389  indifdir  3391  difin2  3397  inrab2  3408  inelcm  3483  inssdif0im  3490  uniin  3829  intun  3875  intpr  3876  elrint  3884  iunin2  3950  iinin2m  3955  elriin  3957  disjnim  3994  disjiun  3998  brin  4055  trin  4111  inex1  4137  inuni  4155  bnd2  4173  ordpwsucss  4566  ordpwsucexmid  4569  peano5  4597  inopab  4759  inxp  4761  dmin  4835  opelres  4912  intasym  5013  asymref  5014  dminss  5043  imainss  5044  inimasn  5046  ssrnres  5071  cnvresima  5118  dfco2a  5129  funinsn  5265  imainlem  5297  imain  5298  2elresin  5327  nfvres  5548  respreima  5644  isoini  5818  offval  6089  tfrlem5  6314  mapval2  6677  ixpin  6722  ssenen  6850  fnfi  6935  peano5nnnn  7890  peano5nni  8921  ixxdisj  9902  icodisj  9991  fzdisj  10051  uzdisj  10092  nn0disj  10137  fzouzdisj  10179  isumss  11398  fsumsplit  11414  sumsplitdc  11439  fsum2dlemstep  11441  fprod2dlemstep  11629  nninfdclemcl  12448  nninfdclemp1  12450  insubm  12871  subsubrg2  13365  isbasis2g  13515  tgval2  13521  tgcl  13534  epttop  13560  ssntr  13592  ntreq0  13602  cnptopresti  13708  cnptoprest  13709  cnptoprest2  13710  lmss  13716  txcnp  13741  txcnmpt  13743  bldisj  13871  blininf  13894  blres  13904  metrest  13976  pilem1  14170  bj-charfundcALT  14531  bj-charfunr  14532  bdinex1  14621  bj-indind  14654