MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  incom Structured version   Unicode version

Theorem incom 3593
Description: Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-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 451 . . 3  |-  ( ( x  e.  A  /\  x  e.  B )  <->  ( x  e.  B  /\  x  e.  A )
)
2 elin 3587 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
3 elin 3587 . . 3  |-  ( x  e.  ( B  i^i  A )  <->  ( x  e.  B  /\  x  e.  A ) )
41, 2, 33bitr4i 280 . 2  |-  ( x  e.  ( A  i^i  B )  <->  x  e.  ( B  i^i  A ) )
54eqriv 2420 1  |-  ( A  i^i  B )  =  ( B  i^i  A
)
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370    = wceq 1437    e. wcel 1872    i^i cin 3373
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-v 3019  df-in 3381
This theorem is referenced by:  ineq2  3596  dfss1  3605  in12  3611  in32  3612  in13  3613  in31  3614  inss2  3621  sslin  3626  inss  3629  indif1  3655  indifcom  3656  indir  3659  dfsymdif3  3676  symdif1OLD  3677  dfrab2  3687  disjr  3774  ssdifin0  3817  difdifdir  3823  uneqdifeq  3824  diftpsn3  4076  iinrab2  4300  iunin1  4302  iinin1  4308  riinn0  4312  rintn0  4331  disjprg  4357  disjxun  4359  inex2  4504  resiun1  5080  dmres  5082  rescom  5086  resima2  5095  xpssres  5096  resindm  5106  resdmdfsn  5107  resopab  5108  imadisj  5144  ndmimaOLD  5163  intirr  5175  djudisj  5221  imainrect  5235  dmresv  5251  resdmres  5283  coeq0  5301  dfpred3  5347  pred0  5367  wfi  5370  ordtri3or  5412  fnresdisj  5642  fnimaeq0  5653  resasplit  5708  fresaun  5709  fresaunres2  5710  fresaunres1  5711  f0rn0  5723  fvun2  5892  fveqressseq  5972  ressnop0  6025  fninfp  6045  fvsnun1  6053  fsnunfv  6058  fveqf1o  6154  orduniss2  6613  offres  6741  curry1  6838  curry2  6841  fpar  6850  fnsuppeq0  6893  wfrlem5  6990  smores3  7022  oacomf1o  7216  ralxpmap  7471  difsnen  7602  domunsncan  7620  domunsn  7670  limensuci  7696  phplem2  7700  pssnn  7738  dif1en  7752  domunfican  7792  marypha1lem  7895  epfrs  8162  zfregs2  8164  tskwe  8331  dif1card  8388  dfac8b  8408  ac10ct  8411  kmlem11  8536  kmlem12  8537  cdacomen  8557  onacda  8573  ackbij1lem14  8609  ackbij1lem16  8611  ackbij1lem18  8613  fin23lem26  8701  fin23lem19  8712  fin23lem30  8718  isf32lem4  8732  isf34lem7  8755  isf34lem6  8756  axdc3lem4  8829  brdom7disj  8905  brdom6disj  8906  fpwwe2lem13  9013  canthp1lem1  9023  grothprim  9205  fzpreddisj  11791  fzdifsuc  11801  fseq1p1m1  11814  hashgval  12463  hashun3  12508  hashfun  12552  hashbclem  12558  xpcoidgend  12978  cotr2  12980  limsupgle  13473  prmreclem2  14799  setsid  15102  ressinbas  15123  wunress  15127  mreexexlem2d  15489  mreexexlem4d  15491  oppcinv  15623  cnvps  16396  pmtrmvd  17035  lsmmod2  17264  lsmdisj3  17271  lsmdisjr  17272  lsmdisj2r  17273  lsmdisj3r  17274  lsmdisj2a  17275  lsmdisj2b  17276  lsmdisj3a  17277  lsmdisj3b  17278  subgdisj2  17280  pj2f  17286  pj1id  17287  frgpuplem  17360  gsummptfzsplitl  17504  dprd2da  17613  dmdprdsplit2lem  17616  dmdprdsplit2  17617  pgpfaclem1  17652  lmhmlsp  18210  pwssplit1  18220  ltbwe  18634  psrbag0  18655  psgndiflemB  19105  pjpm  19208  islindf4  19333  indistopon  19953  fctop  19956  cctop  19958  elcls  20026  mretopd  20045  restin  20119  restsn  20123  restcld  20125  neitr  20133  resstopn  20139  lecldbas  20172  nrmsep  20310  regsep2  20329  isreg2  20330  ordthaus  20337  cmpsublem  20351  cmpsub  20352  hauscmplem  20358  bwth  20362  iuncon  20380  cldllycmp  20447  kgentopon  20490  llycmpkgen2  20502  1stckgen  20506  txkgen  20604  kqcldsat  20685  regr1lem2  20692  fbun  20792  fin1aufil  20884  fclsfnflim  20979  ustexsym  21167  restutopopn  21190  ustuqtop5  21197  ressuss  21215  metreslem  21314  blcld  21457  ressxms  21477  ressms  21478  restmetu  21522  reconn  21783  metdseq0  21808  metnrmlem3  21815  metdseq0OLD  21823  metnrmlem3OLD  21830  unmbl  22428  volun  22435  volinun  22436  iundisj2  22439  icombl  22454  ioombl  22455  uniioombllem2  22477  uniioombllem2OLD  22478  uniioombllem4  22481  dyaddisjlem  22490  dyaddisj  22491  mbfconstlem  22522  mbfeqalem  22535  ismbf3d  22547  itg1addlem5  22595  itgsplitioo  22732  lhop  22905  tdeglem4  22946  vieta1lem2  23201  xrlimcnp  23831  chtdif  24022  ppidif  24027  ppi1  24028  cht1  24029  perfectlem2  24095  rplogsum  24302  perpcom  24695  cusgrasizeindslem2  25139  ex-dif  25810  ococi  26995  orthin  27036  lediri  27127  pjoml2i  27175  pjoml4i  27177  cmcmlem  27181  cmbr3i  27190  cmm2i  27197  cm0  27199  fh1  27208  fh2  27209  cm2j  27210  qlaxr3i  27226  pjclem2  27786  stm1ri  27834  golem1  27861  dmdbr5  27898  mddmd2  27899  cvmdi  27914  mdsldmd1i  27921  csmdsymi  27924  mdexchi  27925  cvexchi  27959  atssma  27968  atomli  27972  atoml2i  27973  atordi  27974  atcvatlem  27975  chirredlem1  27980  chirredlem2  27981  chirredlem3  27982  atcvat4i  27987  atabsi  27991  mdsymlem1  27993  dmdbr6ati  28013  cdj3lem3  28028  inin  28087  difeq  28089  difuncomp  28107  disjdifprg  28126  iundisj2f  28141  disjunsn  28145  imadifxp  28153  fnresin  28169  ofpreima2  28210  df1stres  28225  df2ndres  28226  padct  28252  iocinif  28308  difioo  28309  iundisj2fi  28318  xrge00  28394  xrge0slmod  28554  ordtconlem1  28677  lmxrge0  28705  esumrnmpt2  28836  esumpfinvallem  28842  ldgenpisyslem1  28932  ldgenpisys  28935  measxun2  28979  measvuni  28983  measunl  28985  measinb  28990  carsgclctunlem1  29096  carsgclctunlem2  29098  eulerpartlemt  29151  eulerpartgbij  29152  probmeasb  29210  cndprobnul  29217  bayesth  29219  ballotlemfp1  29271  ballotlemfval0  29275  ballotlemgun  29304  ballotlemgunOLD  29342  signstres  29411  subfacp1lem3  29852  subfacp1lem5  29854  pconcon  29901  cvmscld  29943  cvmsss2  29944  mrsubvrs  30107  mthmpps  30167  frind  30427  frrlem5  30464  nofulllem5  30539  cldbnd  30926  bj-inrab3  31443  bj-2upln1upl  31529  bj-diagval  31552  icoreclin  31667  fin2so  31839  ptrest  31846  poimirlem3  31850  poimirlem11  31858  poimirlem12  31859  poimirlem13  31860  poimirlem14  31861  poimirlem15  31862  poimirlem16  31863  poimirlem18  31865  poimirlem19  31866  poimirlem21  31868  poimirlem22  31869  poimirlem25  31872  poimirlem27  31874  mblfinlem2  31885  mblfinlem3  31886  mblfinlem4  31887  ismblfin  31888  cnambfre  31896  asindmre  31934  dvasin  31935  dvreasin  31937  dvreacos  31938  sstotbnd2  32013  bndss  32025  l1cvat  32533  pmod2iN  33326  pmodN  33327  pmodl42N  33328  osumcllem3N  33435  osumcllem4N  33436  dihmeetlem19N  34805  dihmeetALTN  34807  elrfi  35448  diophrw  35513  eldioph2lem1  35514  eldioph2lem2  35515  diophin  35527  diophren  35568  dnwech  35819  fnwe2lem2  35822  kelac1  35834  kelac2lem  35835  kelac2  35836  lmhmlnmsplit  35858  pwssplit4  35860  pwfi2f1o  35867  proot1hash  35990  rp-fakeuninass  36074  elcnvcnvintab  36101  relintab  36102  elcnvcnvlem  36118  conrel1d  36168  dfrcl2  36179  iunrelexp0  36207  hashnzfz  36582  zfregs2VD  37153  iunconlem2  37248  0in  37309  ssinss2d  37316  iccdifioo  37508  sumnnodd  37593  cncfuni  37647  fouriersw  37978  saliincl  38050  iundjiunlem  38148  iundjiun  38149  caragenuncllem  38184  caragendifcl  38186  isomenndlem  38202  hoidmvlelem2  38265  perfectALTVlem2  38657  rnghmsscmap2  39566  rnghmsubcsetclem1  39568  rnghmsubcsetc  39570  rngccat  39571  rngcid  39572  rngchomrnghmresALTV  39589  rngcifuestrc  39590  funcrngcsetc  39591  rhmsscmap2  39612  rhmsubcsetclem1  39614  rhmsubcsetc  39616  ringccat  39617  ringcid  39618  rhmsscrnghm  39619  rhmsubcrngclem1  39620  rhmsubcrngc  39622  rngcresringcat  39623  funcringcsetc  39628  rngcrescrhm  39678  rhmsubclem3  39681  rhmsubc  39683  rngcrescrhmALTV  39697  rhmsubcALTVlem3  39700  rhmsubcALTVlem4  39701
  Copyright terms: Public domain W3C validator