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  4268  onintexmid  4720  resiun1  5082  dmres  5084  rescom  5088  resima2  5097  xpssres  5098  resindm  5105  resdmdfsn  5106  resopab  5107  imadisj  5149  ndmima  5164  intirr  5174  djudisj  5215  imainrect  5233  dmresv  5246  resdmres  5279  funimaexg  5465  fnresdisj  5493  fnimaeq0  5505  resasplitss  5569  fresaunres1disj  5571  f0rn0  5587  fvun2  5770  ressnop0  5896  fvsnun1  5912  fsnunfv  5916  offres  6368  smores3  6564  phplem2  7154  unfiin  7233  xpfi  7239  endjusym  7436  djucomen  7572  fzpreddisj  10478  fseq1p1m1  10501  hashunlem  11244  hashfibclem  11282  zfz1isolem1  11292  fprodsplit  12364  ballotfilemfval0  13235  znnen  13289  setsfun  13387  setsfun0  13388  setsslid  13403  ressressg  13429  restin  15277  metreslem  15481  perfectlem2  16114  bdinex2  16926