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

Theorem incom 3238
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 3229 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
3 elin 3229 . . 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 2114 1  |-  ( A  i^i  B )  =  ( B  i^i  A
)
Colors of variables: wff set class
Syntax hints:    /\ wa 103    = wceq 1316    e. wcel 1465    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:  ineq2  3241  dfss1  3250  in12  3257  in32  3258  in13  3259  in31  3260  inss2  3267  sslin  3272  inss  3276  indif1  3291  indifcom  3292  indir  3295  symdif1  3311  dfrab2  3321  0in  3368  disjr  3382  ssdifin0  3414  difdifdirss  3417  uneqdifeqim  3418  diftpsn3  3631  iunin1  3847  iinin1m  3852  riinm  3855  rintm  3875  inex2  4033  onintexmid  4457  resiun1  4808  dmres  4810  rescom  4814  resima2  4823  xpssres  4824  resindm  4831  resdmdfsn  4832  resopab  4833  imadisj  4871  ndmima  4886  intirr  4895  djudisj  4936  imainrect  4954  dmresv  4967  resdmres  5000  funimaexg  5177  fnresdisj  5203  fnimaeq0  5214  resasplitss  5272  f0rn0  5287  fvun2  5456  ressnop0  5569  fvsnun1  5585  fsnunfv  5589  offres  6001  smores3  6158  phplem2  6715  unfiin  6782  xpfi  6786  endjusym  6949  djucomen  7040  fzpreddisj  9819  fseq1p1m1  9842  hashunlem  10518  zfz1isolem1  10551  znnen  11838  setsfun  11921  setsfun0  11922  setsslid  11936  restin  12272  metreslem  12476  bdinex2  13025
  Copyright terms: Public domain W3C validator