ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elin Unicode version

Theorem elin 3263
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.
StepHypRef Expression
1 elex 2700 . 2  |-  ( A  e.  ( B  i^i  C )  ->  A  e.  _V )
2 elex 2700 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32adantl 275 . 2  |-  ( ( A  e.  B  /\  A  e.  C )  ->  A  e.  _V )
4 eleq1 2203 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2203 . . . 4  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
64, 5anbi12d 465 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  x  e.  C
)  <->  ( A  e.  B  /\  A  e.  C ) ) )
7 df-in 3081 . . 3  |-  ( B  i^i  C )  =  { x  |  ( x  e.  B  /\  x  e.  C ) }
86, 7elab2g 2834 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) ) )
91, 3, 8pm5.21nii 694 1  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104    = wceq 1332    e. wcel 1481   _Vcvv 2689    i^i cin 3074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-in 3081
This theorem is referenced by:  elini  3264  elind  3265  elinel1  3266  elinel2  3267  elin2  3268  elin3  3271  incom  3272  ineqri  3273  ineq1  3274  inass  3290  inss1  3300  ssin  3302  ssrin  3305  dfss4st  3313  inssdif  3316  difin  3317  unssin  3319  inssun  3320  invdif  3322  indif  3323  indi  3327  undi  3328  difundi  3332  difindiss  3334  indifdir  3336  difin2  3342  inrab2  3353  inelcm  3427  inssdif0im  3434  uniin  3763  intun  3809  intpr  3810  elrint  3818  iunin2  3883  iinin2m  3888  elriin  3890  disjnim  3927  disjiun  3931  brin  3987  trin  4043  inex1  4069  inuni  4087  bnd2  4104  ordpwsucss  4489  ordpwsucexmid  4492  peano5  4519  inopab  4678  inxp  4680  dmin  4754  opelres  4831  intasym  4930  asymref  4931  dminss  4960  imainss  4961  inimasn  4963  ssrnres  4988  cnvresima  5035  dfco2a  5046  funinsn  5179  imainlem  5211  imain  5212  2elresin  5241  nfvres  5461  respreima  5555  isoini  5726  offval  5996  tfrlem5  6218  mapval2  6579  ixpin  6624  ssenen  6752  fnfi  6832  peano5nnnn  7723  peano5nni  8746  ixxdisj  9715  icodisj  9804  fzdisj  9862  uzdisj  9903  nn0disj  9945  fzouzdisj  9987  isumss  11191  fsumsplit  11207  sumsplitdc  11232  fsum2dlemstep  11234  isbasis2g  12249  tgval2  12257  tgcl  12270  epttop  12296  ssntr  12328  ntreq0  12338  cnptopresti  12444  cnptoprest  12445  cnptoprest2  12446  lmss  12452  txcnp  12477  txcnmpt  12479  bldisj  12607  blininf  12630  blres  12640  metrest  12712  pilem1  12906  bdinex1  13266  bj-indind  13299
  Copyright terms: Public domain W3C validator