Theorem incom 3328

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 3319	. . 3 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
3		elin 3319	. . 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 2174	1 |- ( A i^i B ) = ( B i^i A )

Syntax hints:   /\ wa 104   = wceq 1353   e. wcel 2148   i^i cin 3129

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-in 3136

This theorem is referenced by:  ineq2  3331  dfss1  3340  in12  3347  in32  3348  in13  3349  in31  3350  inss2  3357  sslin  3362  inss  3366  indif1  3381  indifcom  3382  indir  3385  symdif1  3401  dfrab2  3411  0in  3459  disjr  3473  ssdifin0  3505  difdifdirss  3508  uneqdifeqim  3509  diftpsn3  3734  iunin1  3952  iinin1m  3957  riinm  3960  rintm  3980  inex2  4139  onintexmid  4573  resiun1  4927  dmres  4929  rescom  4933  resima2  4942  xpssres  4943  resindm  4950  resdmdfsn  4951  resopab  4952  imadisj  4991  ndmima  5006  intirr  5016  djudisj  5057  imainrect  5075  dmresv  5088  resdmres  5121  funimaexg  5301  fnresdisj  5327  fnimaeq0  5338  resasplitss  5396  f0rn0  5411  fvun2  5584  ressnop0  5698  fvsnun1  5714  fsnunfv  5718  offres  6136  smores3  6294  phplem2  6853  unfiin  6925  xpfi  6929  endjusym  7095  djucomen  7215  fzpreddisj  10071  fseq1p1m1  10094  hashunlem  10784  zfz1isolem1  10820  fprodsplit  11605  znnen  12399  setsfun  12497  setsfun0  12498  setsslid  12513  ressressg  12534  restin  13679  metreslem  13883  bdinex2  14655