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

Theorem incom 3310
Description: Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
incom  |-  ( A  i^i  B )  =  ( B  i^i  A
)

Proof of Theorem incom
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 ancom 264 . . 3  |-  ( ( x  e.  A  /\  x  e.  B )  <->  ( x  e.  B  /\  x  e.  A )
)
2 elin 3301 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
3 elin 3301 . . 3  |-  ( x  e.  ( B  i^i  A )  <->  ( x  e.  B  /\  x  e.  A ) )
41, 2, 33bitr4i 211 . 2  |-  ( x  e.  ( A  i^i  B )  <->  x  e.  ( B  i^i  A ) )
54eqriv 2161 1  |-  ( A  i^i  B )  =  ( B  i^i  A
)
Colors of variables: wff set class
Syntax hints:    /\ wa 103    = wceq 1342    e. wcel 2135    i^i cin 3111
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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146
This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2724  df-in 3118
This theorem is referenced by:  ineq2  3313  dfss1  3322  in12  3329  in32  3330  in13  3331  in31  3332  inss2  3339  sslin  3344  inss  3348  indif1  3363  indifcom  3364  indir  3367  symdif1  3383  dfrab2  3393  0in  3440  disjr  3454  ssdifin0  3486  difdifdirss  3489  uneqdifeqim  3490  diftpsn3  3709  iunin1  3925  iinin1m  3930  riinm  3933  rintm  3953  inex2  4112  onintexmid  4545  resiun1  4898  dmres  4900  rescom  4904  resima2  4913  xpssres  4914  resindm  4921  resdmdfsn  4922  resopab  4923  imadisj  4961  ndmima  4976  intirr  4985  djudisj  5026  imainrect  5044  dmresv  5057  resdmres  5090  funimaexg  5267  fnresdisj  5293  fnimaeq0  5304  resasplitss  5362  f0rn0  5377  fvun2  5548  ressnop0  5661  fvsnun1  5677  fsnunfv  5681  offres  6096  smores3  6253  phplem2  6811  unfiin  6883  xpfi  6887  endjusym  7053  djucomen  7164  fzpreddisj  9997  fseq1p1m1  10020  hashunlem  10707  zfz1isolem1  10743  fprodsplit  11528  znnen  12294  setsfun  12392  setsfun0  12393  setsslid  12407  restin  12743  metreslem  12947  bdinex2  13644
  Copyright terms: Public domain W3C validator