Theorem incom 3449

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.

Step	Hyp	Ref	Expression
1		ancom 437	. . 3 |- ((x e. A /\ x e. B) <-> (x e. B /\ x e. A))
2		elin 3220	. . 3 |- (x e. (A i^i B) <-> (x e. A /\ x e. B))
3		elin 3220	. . 3 |- (x e. (B i^i A) <-> (x e. B /\ x e. A))
4	1, 2, 3	3bitr4i 268	. 2 |- (x e. (A i^i B) <-> x e. (B i^i A))
5	4	eqriv 2350	1 |- (A i^i B) = (B i^i A)

Syntax hints:   /\ wa 358   = wceq 1642   e. wcel 1710   i^i cin 3209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214

This theorem is referenced by:  ineq2  3452  dfss1  3461  in12  3467  in32  3468  in13  3469  in31  3470  inss2  3477  sslin  3482  inss  3485  indif1  3500  indifcom  3501  indir  3504  symdif1  3520  dfrab2  3531  disjr  3593  ssdifin0  3632  difdifdir  3638  uneqdifeq  3639  diftpsn3  3850  iinrab2  4030  iunin1  4032  iinin1  4038  riinn0  4041  rintn0  4057  compldif  4070  xpkexg  4289  dfiota4  4373  dfaddc2  4382  addccom  4407  nndisjeq  4430  phialllem2  4618  dmres  4987  rescom  4990  resabs1  4993  resopab  5000  imadisj  5016  ndmima  5026  intirr  5030  resdmres  5079  funun  5147  fnresdisj  5194  fvun2  5381  ressnop0  5437  fvsnun1  5448  enadj  6061  nchoicelem7  6296  nchoicelem14  6303