Theorem incom 3314

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 264	. . 3 |- ( ( x e. A /\ x e. B ) <-> ( x e. B /\ x e. A ) )
2		elin 3305	. . 3 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
3		elin 3305	. . 3 |- ( x e. ( B i^i A ) <-> ( x e. B /\ x e. A ) )
4	1, 2, 3	3bitr4i 211	. 2 |- ( x e. ( A i^i B ) <-> x e. ( B i^i A ) )
5	4	eqriv 2162	1 |- ( A i^i B ) = ( B i^i A )

Syntax hints:   /\ wa 103   = wceq 1343   e. wcel 2136   i^i cin 3115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-in 3122

This theorem is referenced by:  ineq2  3317  dfss1  3326  in12  3333  in32  3334  in13  3335  in31  3336  inss2  3343  sslin  3348  inss  3352  indif1  3367  indifcom  3368  indir  3371  symdif1  3387  dfrab2  3397  0in  3444  disjr  3458  ssdifin0  3490  difdifdirss  3493  uneqdifeqim  3494  diftpsn3  3714  iunin1  3930  iinin1m  3935  riinm  3938  rintm  3958  inex2  4117  onintexmid  4550  resiun1  4903  dmres  4905  rescom  4909  resima2  4918  xpssres  4919  resindm  4926  resdmdfsn  4927  resopab  4928  imadisj  4966  ndmima  4981  intirr  4990  djudisj  5031  imainrect  5049  dmresv  5062  resdmres  5095  funimaexg  5272  fnresdisj  5298  fnimaeq0  5309  resasplitss  5367  f0rn0  5382  fvun2  5553  ressnop0  5666  fvsnun1  5682  fsnunfv  5686  offres  6103  smores3  6261  phplem2  6819  unfiin  6891  xpfi  6895  endjusym  7061  djucomen  7172  fzpreddisj  10006  fseq1p1m1  10029  hashunlem  10717  zfz1isolem1  10753  fprodsplit  11538  znnen  12331  setsfun  12429  setsfun0  12430  setsslid  12444  restin  12816  metreslem  13020  bdinex2  13782