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

Theorem elin 3229
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 2671 . 2  |-  ( A  e.  ( B  i^i  C )  ->  A  e.  _V )
2 elex 2671 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32adantl 275 . 2  |-  ( ( A  e.  B  /\  A  e.  C )  ->  A  e.  _V )
4 eleq1 2180 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2180 . . . 4  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
64, 5anbi12d 464 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  x  e.  C
)  <->  ( A  e.  B  /\  A  e.  C ) ) )
7 df-in 3047 . . 3  |-  ( B  i^i  C )  =  { x  |  ( x  e.  B  /\  x  e.  C ) }
86, 7elab2g 2804 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) ) )
91, 3, 8pm5.21nii 678 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 1316    e. wcel 1465   _Vcvv 2660    i^i cin 3040
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-in 3047
This theorem is referenced by:  elini  3230  elind  3231  elinel1  3232  elinel2  3233  elin2  3234  elin3  3237  incom  3238  ineqri  3239  ineq1  3240  inass  3256  inss1  3266  ssin  3268  ssrin  3271  dfss4st  3279  inssdif  3282  difin  3283  unssin  3285  inssun  3286  invdif  3288  indif  3289  indi  3293  undi  3294  difundi  3298  difindiss  3300  indifdir  3302  difin2  3308  inrab2  3319  inelcm  3393  inssdif0im  3400  uniin  3726  intun  3772  intpr  3773  elrint  3781  iunin2  3846  iinin2m  3851  elriin  3853  disjnim  3890  disjiun  3894  brin  3950  trin  4006  inex1  4032  inuni  4050  bnd2  4067  ordpwsucss  4452  ordpwsucexmid  4455  peano5  4482  inopab  4641  inxp  4643  dmin  4717  opelres  4794  intasym  4893  asymref  4894  dminss  4923  imainss  4924  inimasn  4926  ssrnres  4951  cnvresima  4998  dfco2a  5009  funinsn  5142  imainlem  5174  imain  5175  2elresin  5204  nfvres  5422  respreima  5516  isoini  5687  offval  5957  tfrlem5  6179  mapval2  6540  ixpin  6585  ssenen  6713  fnfi  6793  peano5nnnn  7668  peano5nni  8687  ixxdisj  9641  icodisj  9730  fzdisj  9787  uzdisj  9828  nn0disj  9870  fzouzdisj  9912  isumss  11115  fsumsplit  11131  sumsplitdc  11156  fsum2dlemstep  11158  isbasis2g  12123  tgval2  12131  tgcl  12144  epttop  12170  ssntr  12202  ntreq0  12212  cnptopresti  12318  cnptoprest  12319  cnptoprest2  12320  lmss  12326  txcnp  12351  txcnmpt  12353  bldisj  12481  blininf  12504  blres  12514  metrest  12586  pilem1  12771  bdinex1  12993  bj-indind  13026
  Copyright terms: Public domain W3C validator