Theorem incom 3421

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

This proof depends on syntax axioms:   /\ wa 104   = wceq 1402   e. wcel 2209   i^i cin 3219

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226

This theorem is used by:  ineqcom  3422  ineqcomi  3423  ineq2  3426  dfss1  3435  in12  3442  in32  3443  in13  3444  in31  3445  inss2  3452  sslin  3457  inss  3461  indif1  3476  indifcom  3477  indir  3480  symdif1  3496  dfrab2  3508  0in  3558  disjr  3574  ssdifin0  3609  difdifdirss  3612  uneqdifeqim  3613  diftpsn3  3856  iunin1  4077  iinin1m  4082  riinm  4085  rintm  4105  inex2  4270  onintexmid  4722  resiun1  5084  dmres  5086  rescom  5090  resima2  5099  xpssres  5100  resindm  5108  resdmdfsn  5109  resopab  5110  imadisj  5152  ndmima  5167  intirr  5177  djudisj  5218  imainrect  5236  dmresv  5249  resdmres  5282  funimaexg  5468  fnresdisj  5496  fnimaeq0  5508  resasplitss  5572  fresaunres1disj  5574  f0rn0  5590  fvun2  5773  ressnop0  5899  fvsnun1  5915  fsnunfv  5919  offres  6372  smores3  6568  phplem2  7158  unfiin  7237  xpfi  7243  endjusym  7442  djucomen  7578  fzpreddisj  10495  fseq1p1m1  10518  hashunlem  11266  hashfibclem  11304  zfz1isolem1  11314  fprodsplit  12389  ballotfilemfval0  13293  znnen  13347  setsfun  13445  setsfun0  13446  setsslid  13461  ressressg  13488  restin  15402  metreslem  15606  perfectlem2  16300  bdinex2  17131