Theorem incom 2787

Description: Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17.

Assertion

Ref	Expression
incom	|- (A i^i B) = (B i^i A)

Proof of Theorem incom

Step	Hyp	Ref	Expression
1		ancom 482	. . 3 |- ((x e. A /\ x e. B) <-> (x e. B /\ x e. A))
2		elin 2786	. . 3 |- (x e. (A i^i B) <-> (x e. A /\ x e. B))
3		elin 2786	. . 3 |- (x e. (B i^i A) <-> (x e. B /\ x e. A))
4	1, 2, 3	3bitr4i 200	. 2 |- (x e. (A i^i B) <-> x e. (B i^i A))
5	4	eqriv 1881	1 |- (A i^i B) = (B i^i A)

Syntax hints:   /\ wa 240   = wceq 1298   e. wcel 1300   i^i cin 2592

This theorem is referenced by:  ineq2 2790  in12 2805  in23 2806  in23OLD 2807  sseqin2 2811  inss2 2813  sslin 2819  indir 2842  symdif1 2856  dfrab2 2869  difdifdir 2957  iinrab2 3319  2iunin 3323  inex2 3453  ordtri3or 3691  ordtri3orOLD 3692  orduniss2 3913  onnev 4070  dmres 4234  rescom 4238  resopab 4252  imadisj 4285  ndmima 4300  intirr 4312  dmsnn0OLD 4363  dmresv 4382  rescnvcnvOLD 4386  resdmres 4390  fnresdisj 4523  fvsnun1 4764  curry1 5075  curry2 5078  fpar 5085  mapdom2lem 5587  mapunen 5596  limensuci 5600  phplem2 5603  pssnn 5628  zfreg2 5699  zfregs 5754  zfregs2 5755  kmlem11 5937  kmlem12 5938  brdom7disj 5966  brdom6disj 5967  subtop 8916  indistop 8918  fctop 8920  cctop 8922  elcls 8980  islp2 9023  qdensere 9027  cnconst 9057  metssba 9086  metssba2 9087  lpbl 9157  lmsslem 9230  lmss 9231  bcthlem9 9285  grothprim 10141  twpar2 10149  dif1en 10172  stoiglem 10250  subcld 10254  extbas1 10291  sfvlim 10296  ococi 10880  orthin 11003  chjoi 11044  lediri 11093  pjoml2i 11161  pjoml4i 11163  cmcmlem 11167  cmbr3i 11176  cmm2i 11183  cm0 11185  fh1 11194  fh2 11195  cm2j 11196  qlaxr3i 11212  dfbdop2 11423  pjclem2 11769  stm1ri 11816  golem1 11843  dmdbr5 11880  mddmd2 11881  cvmdi 11896  mdsldmd1i 11903  csmdsymi 11906  mdexchi 11907  cvexchi 11941  atssma 11950  atomli 11954  atoml2i 11955  atordi 11956  atcvatlem 11957  irredlem1 11962  irredlem2 11963  irredlem3 11964  atcvat4i 11969  atabsi 11973  mdsymlem1 11975  dmdbr6ati 11995  cdj3lem3 12010  bnj1250 13015  fresin 13840  epsetlike 13905  pred0 13910  wfi 13915  frind 13939  wfrlem5 13961  dfoprab4spop 14339  uninqs 14340  infi1 14343  inpws2 14346  moec 14351  neiopne 14354  imrescl 14393  repfuntw 14502  domrancur1b 14548  domrancur1c 14550  dupos1 14586  inposet 14620  ranncnt 14625  sbtpsines 14905  subtopsin2 14907  cnfilca 14927  bwt2 14960  clindistop 14962  stoi 14998  inttaror 15277  carinttar 15279  cartarlim 15282  fictb 15371  cldbnd 15410  subsubtop 15423  compsublem 15430  compsub 15431  connsub 15443  reconn 15451  locfincomp 15514  isnrm2 15552  filcon 15580  fclsfnflim 15614  disjr 15675  bndss 15942  heiborlem11 15965  smores2 16447  zfregs2VD 16665  pmod2i 17310  pmod 17311  pmodl42 17312  osumcllem3 17366  osumcllem4 17367

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-in 2603

Copyright terms: Public domain