Theorem incom 2205

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 435	. . 3 |- ((x e. A /\ x e. B) <-> (x e. B /\ x e. A))
2		elin 2204	. . 3 |- (x e. (A i^i B) <-> (x e. A /\ x e. B))
3		elin 2204	. . 3 |- (x e. (B i^i A) <-> (x e. B /\ x e. A))
4	1, 2, 3	3bitr4 183	. 2 |- (x e. (A i^i B) <-> x e. (B i^i A))
5	4	eqriv 1473	1 |- (A i^i B) = (B i^i A)

Syntax hints:   /\ wa 223   = wceq 955   e. wcel 957   i^i cin 2043

This theorem is referenced by:  ineq2 2208  in12 2221  in23 2222  sseqin2 2226  inss2 2228  sslin 2232  indir 2250  symdif1 2262  dfrab2 2271  difdifdir 2343  inex2 2713  ordtri3or 2975  orduniss2 3086  onnev 3238  dmres 3376  rescom 3380  resopab 3391  imadisj 3418  ndmima 3430  dmresv 3486  rescnvcnv 3489  resdmres 3493  fnresdisj 3593  fvsnun1 3790  curry1 4091  mapdom2lem 4482  mapunen 4491  limensuci 4495  phplem2 4498  pssnn 4522  zfreg2 4580  zfregs 4630  kmlem11 4758  kmlem12 4759  brdom7disj 4787  brdom6disj 4788  subtop 7606  indistop 7608  fctop 7610  cctop 7612  elcls 7664  islp2 7707  qdensere 7711  cnconst 7740  metssba 7769  metssba2 7770  lpbl 7842  lmsslem 7914  lmss 7915  bcthlem9 7969  grothprim 8738  ococ 9202  orthin 9325  chjo 9366  ledir 9415  pjoml2 9485  pjoml4 9487  cmcmlem 9491  cmbr3 9500  cmm2 9507  cm0t 9509  fh1t 9518  fh2t 9519  cm2jt 9520  qlaxr3 9534  dfbdop2 9743  pjclem2 10080  stm1r 10127  golem1 10154  dmdbr5 10191  mddmd 10192  cvmd 10207  mdsldmd1 10214  csmdsym 10217  mdexch 10218  cvexch 10252  atssmat 10261  atoml 10265  atoml2 10266  atord 10267  atcvatlem 10268  irredlem1 10273  irredlem2 10274  irredlem3 10275  atcvat4 10280  atabs 10284  mdsymlem1 10286  dmdbr6at 10306  cdj3lem3 10321  uninqs 10400  infi1 10405  inpws2 10410  moec 10415  neiopne 10427  cnfilca 10510  sfvlim 10522  stoi 10555

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809  df-in 2048

Copyright terms: Public domain