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

Theorem incom 3165
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 262 . . 3  |-  ( ( x  e.  A  /\  x  e.  B )  <->  ( x  e.  B  /\  x  e.  A )
)
2 elin 3156 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
3 elin 3156 . . 3  |-  ( x  e.  ( B  i^i  A )  <->  ( x  e.  B  /\  x  e.  A ) )
41, 2, 33bitr4i 210 . 2  |-  ( x  e.  ( A  i^i  B )  <->  x  e.  ( B  i^i  A ) )
54eqriv 2079 1  |-  ( A  i^i  B )  =  ( B  i^i  A
)
Colors of variables: wff set class
Syntax hints:    /\ wa 102    = wceq 1285    e. wcel 1434    i^i cin 2973
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-in 2980
This theorem is referenced by:  ineq2  3168  dfss1  3177  in12  3184  in32  3185  in13  3186  in31  3187  inss2  3194  sslin  3199  inss  3202  indif1  3216  indifcom  3217  indir  3220  symdif1  3236  dfrab2  3246  disjr  3300  ssdifin0  3331  difdifdirss  3334  uneqdifeqim  3335  diftpsn3  3535  iunin1  3750  iinin1m  3755  riinm  3758  rintm  3773  inex2  3921  onintexmid  4323  resiun1  4658  dmres  4660  rescom  4664  resima2  4672  xpssres  4673  resindm  4680  resdmdfsn  4681  resopab  4682  imadisj  4717  ndmima  4732  intirr  4741  djudisj  4780  imainrect  4796  dmresv  4809  resdmres  4842  funimaexg  5014  fnresdisj  5040  fnimaeq0  5051  resasplitss  5100  fvun2  5272  ressnop0  5376  fvsnun1  5392  fsnunfv  5395  offres  5793  smores3  5942  phplem2  6388  unfiin  6444  fzpreddisj  9164  fseq1p1m1  9187  sizeunlem  9828  znnen  10709  bdinex2  10849
  Copyright terms: Public domain W3C validator