Theorem incom 3319

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

Syntax hints:   /\ wa 103   = wceq 1348   e. wcel 2141   i^i cin 3120

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127

This theorem is referenced by:  ineq2  3322  dfss1  3331  in12  3338  in32  3339  in13  3340  in31  3341  inss2  3348  sslin  3353  inss  3357  indif1  3372  indifcom  3373  indir  3376  symdif1  3392  dfrab2  3402  0in  3450  disjr  3464  ssdifin0  3496  difdifdirss  3499  uneqdifeqim  3500  diftpsn3  3721  iunin1  3937  iinin1m  3942  riinm  3945  rintm  3965  inex2  4124  onintexmid  4557  resiun1  4910  dmres  4912  rescom  4916  resima2  4925  xpssres  4926  resindm  4933  resdmdfsn  4934  resopab  4935  imadisj  4973  ndmima  4988  intirr  4997  djudisj  5038  imainrect  5056  dmresv  5069  resdmres  5102  funimaexg  5282  fnresdisj  5308  fnimaeq0  5319  resasplitss  5377  f0rn0  5392  fvun2  5563  ressnop0  5677  fvsnun1  5693  fsnunfv  5697  offres  6114  smores3  6272  phplem2  6831  unfiin  6903  xpfi  6907  endjusym  7073  djucomen  7193  fzpreddisj  10027  fseq1p1m1  10050  hashunlem  10739  zfz1isolem1  10775  fprodsplit  11560  znnen  12353  setsfun  12451  setsfun0  12452  setsslid  12466  restin  12970  metreslem  13174  bdinex2  13935