Theorem incom 3356

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 266	. . 3 |- ( ( x e. A /\ x e. B ) <-> ( x e. B /\ x e. A ) )
2		elin 3347	. . 3 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
3		elin 3347	. . 3 |- ( x e. ( B i^i A ) <-> ( x e. B /\ x e. A ) )
4	1, 2, 3	3bitr4i 212	. 2 |- ( x e. ( A i^i B ) <-> x e. ( B i^i A ) )
5	4	eqriv 2193	1 |- ( A i^i B ) = ( B i^i A )

Syntax hints:   /\ wa 104   = wceq 1364   e. wcel 2167   i^i cin 3156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-in 3163

This theorem is referenced by:  ineq2  3359  dfss1  3368  in12  3375  in32  3376  in13  3377  in31  3378  inss2  3385  sslin  3390  inss  3394  indif1  3409  indifcom  3410  indir  3413  symdif1  3429  dfrab2  3439  0in  3487  disjr  3501  ssdifin0  3533  difdifdirss  3536  uneqdifeqim  3537  diftpsn3  3764  iunin1  3982  iinin1m  3987  riinm  3990  rintm  4010  inex2  4169  onintexmid  4610  resiun1  4966  dmres  4968  rescom  4972  resima2  4981  xpssres  4982  resindm  4989  resdmdfsn  4990  resopab  4991  imadisj  5032  ndmima  5047  intirr  5057  djudisj  5098  imainrect  5116  dmresv  5129  resdmres  5162  funimaexg  5343  fnresdisj  5371  fnimaeq0  5382  resasplitss  5440  f0rn0  5455  fvun2  5631  ressnop0  5746  fvsnun1  5762  fsnunfv  5766  offres  6201  smores3  6360  phplem2  6923  unfiin  6996  xpfi  7002  endjusym  7171  djucomen  7299  fzpreddisj  10163  fseq1p1m1  10186  hashunlem  10913  zfz1isolem1  10949  fprodsplit  11779  znnen  12640  setsfun  12738  setsfun0  12739  setsslid  12754  ressressg  12778  restin  14496  metreslem  14700  perfectlem2  15320  bdinex2  15630