Theorem incom 3273

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

Syntax hints:   /\ wa 103   = wceq 1332   e. wcel 1481   i^i cin 3075

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-in 3082

This theorem is referenced by:  ineq2  3276  dfss1  3285  in12  3292  in32  3293  in13  3294  in31  3295  inss2  3302  sslin  3307  inss  3311  indif1  3326  indifcom  3327  indir  3330  symdif1  3346  dfrab2  3356  0in  3403  disjr  3417  ssdifin0  3449  difdifdirss  3452  uneqdifeqim  3453  diftpsn3  3669  iunin1  3885  iinin1m  3890  riinm  3893  rintm  3913  inex2  4071  onintexmid  4495  resiun1  4846  dmres  4848  rescom  4852  resima2  4861  xpssres  4862  resindm  4869  resdmdfsn  4870  resopab  4871  imadisj  4909  ndmima  4924  intirr  4933  djudisj  4974  imainrect  4992  dmresv  5005  resdmres  5038  funimaexg  5215  fnresdisj  5241  fnimaeq0  5252  resasplitss  5310  f0rn0  5325  fvun2  5496  ressnop0  5609  fvsnun1  5625  fsnunfv  5629  offres  6041  smores3  6198  phplem2  6755  unfiin  6822  xpfi  6826  endjusym  6989  djucomen  7089  fzpreddisj  9882  fseq1p1m1  9905  hashunlem  10582  zfz1isolem1  10615  znnen  11947  setsfun  12033  setsfun0  12034  setsslid  12048  restin  12384  metreslem  12588  bdinex2  13269