Theorem incom 1636

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 333	. . 3 |- ((x e. A /\ x e. B) <-> (x e. B /\ x e. A))
2		elin 1635	. . 3 |- (x e. (A i^i B) <-> (x e. A /\ x e. B))
3		elin 1635	. . 3 |- (x e. (B i^i A) <-> (x e. B /\ x e. A))
4	1, 2, 3	3bitr4 158	. 2 |- (x e. (A i^i B) <-> x e. (B i^i A))
5	4	cleqri 1101	1 |- (A i^i B) = (B i^i A)

Syntax hints:   /\ wa 196   = wceq 1091   e. wcel 1092   i^i cin 1486

This theorem is referenced by:  ineq2 1639  in12 1651  in23 1652  sseqin2 1656  inss2 1658  sslin 1662  indir 1678  symdif1 1689  dfrab2 1696  inex2 1698  difdifdir 1765  ordtri3or 2230  dmres 2584  resopab 2598  ndmima 2623  fnresdisj 2732  mapdom2lem 3388  mapunen 3397  limensuci 3401  phplem3 3405  pssnn 3428  zfreg2 3448  zfregs 3491  kmlem10 3589  kmlem11 3590  facnnt 4870  ruclem7 4891  ococ 5252  pjococ 5272  orthin 5371  chjo 5409  pjoml2 5495  pjoml4 5497  cmcmlem 5500  cmbr3 5509  cmm2 5515  fh1 5518  fh2 5519  qlaxr3 5529  pjclem2 5650  stm1r 5685  golem1 5704  cvexch 5760  atcvatlem 5770  atcvat4 5775  mdsymlem1 5776

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-in 1491

metamath.org