Theorem incom 3448

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 3219	. . 3 |- (x e. (A i^i B) <-> (x e. A /\ x e. B))
3		elin 3219	. . 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 3208

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 2478  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213

This theorem is referenced by:  ineq2  3451  dfss1  3460  in12  3466  in32  3467  in13  3468  in31  3469  inss2  3476  sslin  3481  inss  3484  indif1  3499  indifcom  3500  indir  3503  symdif1  3519  dfrab2  3530  disjr  3592  ssdifin0  3631  difdifdir  3637  uneqdifeq  3638  diftpsn3  3849  iinrab2  4029  iunin1  4031  iinin1  4037  riinn0  4040  rintn0  4056  compldif  4069  xpkexg  4288  dfiota4  4372  dfaddc2  4381  addccom  4406  nndisjeq  4429  phialllem2  4617  dmres  4986  rescom  4989  resabs1  4992  resopab  4999  imadisj  5015  ndmima  5025  intirr  5029  resdmres  5078  funun  5146  fnresdisj  5193  fvun2  5380  ressnop0  5436  fvsnun1  5447  enadj  6060  nchoicelem7  6295  nchoicelem14  6302