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

Theorem elin 3154
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 2583 . 2  |-  ( A  e.  ( B  i^i  C )  ->  A  e.  _V )
2 elex 2583 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32adantl 266 . 2  |-  ( ( A  e.  B  /\  A  e.  C )  ->  A  e.  _V )
4 eleq1 2116 . . . 4  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
5 eleq1 2116 . . . 4  |-  ( x  =  A  ->  (
x  e.  C  <->  A  e.  C ) )
64, 5anbi12d 450 . . 3  |-  ( x  =  A  ->  (
( x  e.  B  /\  x  e.  C
)  <->  ( A  e.  B  /\  A  e.  C ) ) )
7 df-in 2952 . . 3  |-  ( B  i^i  C )  =  { x  |  ( x  e.  B  /\  x  e.  C ) }
86, 7elab2g 2712 . 2  |-  ( A  e.  _V  ->  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) ) )
91, 3, 8pm5.21nii 630 1  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 101    <-> wb 102    = wceq 1259    e. wcel 1409   _Vcvv 2574    i^i cin 2944
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-in 2952
This theorem is referenced by:  elin2  3155  elin3  3156  incom  3157  ineqri  3158  ineq1  3159  inass  3175  inss1  3185  ssin  3187  ssrin  3190  inssdif  3201  difin  3202  unssin  3204  inssun  3205  invdif  3207  indif  3208  indi  3212  undi  3213  difundi  3217  difindiss  3219  indifdir  3221  difin2  3227  inrab2  3238  inelcm  3310  inssdif0im  3319  uniin  3628  intun  3674  intpr  3675  elrint  3683  iunin2  3748  iinin2m  3753  elriin  3755  brin  3839  trin  3892  inex1  3919  inuni  3937  bnd2  3954  ordpwsucss  4319  ordpwsucexmid  4322  peano5  4349  inopab  4496  inxp  4498  dmin  4571  opelres  4645  intasym  4737  asymref  4738  dminss  4766  imainss  4767  inimasn  4769  ssrnres  4791  cnvresima  4838  dfco2a  4849  imainlem  5008  imain  5009  2elresin  5038  nfvres  5234  respreima  5323  isoini  5485  offval  5747  tfrlem5  5961  peano5nnnn  7024  peano5nni  7993  ixxdisj  8873  icodisj  8961  fzdisj  9018  uzdisj  9057  nn0disj  9097  fzouzdisj  9138  bdinex1  10406  bj-indind  10443  peano5setOLD  10452
  Copyright terms: Public domain W3C validator