Theorem elin 3172

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 2624	. 2 |- ( A e. ( B i^i C ) -> A e. _V )
2		elex 2624	. . 3 |- ( A e. C -> A e. _V )
3	2	adantl 271	. 2 |- ( ( A e. B /\ A e. C ) -> A e. _V )
4		eleq1 2147	. . . 4 |- ( x = A -> ( x e. B <-> A e. B ) )
5		eleq1 2147	. . . 4 |- ( x = A -> ( x e. C <-> A e. C ) )
6	4, 5	anbi12d 457	. . 3 |- ( x = A -> ( ( x e. B /\ x e. C ) <-> ( A e. B /\ A e. C ) ) )
7		df-in 2994	. . 3 |- ( B i^i C ) = { x | ( x e. B /\ x e. C ) }
8	6, 7	elab2g 2753	. 2 |- ( A e. _V -> ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) ) )
9	1, 3, 8	pm5.21nii 653	1 |- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )

Syntax hints:   /\ wa 102   <-> wb 103   = wceq 1287   e. wcel 1436   _Vcvv 2615   i^i cin 2987

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-in 2994

This theorem is referenced by:  elini  3173  elind  3174  elinel1  3175  elinel2  3176  elin2  3177  elin3  3180  incom  3181  ineqri  3182  ineq1  3183  inass  3199  inss1  3209  ssin  3211  ssrin  3214  dfss4st  3221  inssdif  3224  difin  3225  unssin  3227  inssun  3228  invdif  3230  indif  3231  indi  3235  undi  3236  difundi  3240  difindiss  3242  indifdir  3244  difin2  3250  inrab2  3261  inelcm  3331  inssdif0im  3338  uniin  3656  intun  3702  intpr  3703  elrint  3711  iunin2  3776  iinin2m  3781  elriin  3783  brin  3867  trin  3921  inex1  3948  inuni  3966  bnd2  3983  ordpwsucss  4356  ordpwsucexmid  4359  peano5  4386  inopab  4536  inxp  4538  dmin  4612  opelres  4686  intasym  4783  asymref  4784  dminss  4812  imainss  4813  inimasn  4815  ssrnres  4839  cnvresima  4886  dfco2a  4897  funinsn  5028  imainlem  5060  imain  5061  2elresin  5090  nfvres  5300  respreima  5390  isoini  5558  offval  5820  tfrlem5  6033  mapval2  6387  ssenen  6519  fnfi  6596  peano5nnnn  7371  peano5nni  8360  ixxdisj  9253  icodisj  9341  fzdisj  9398  uzdisj  9437  nn0disj  9477  fzouzdisj  9519  isumss  10669  bdinex1  11228  bj-indind  11265