Theorem incom 3181

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 262	. . 3 |- ( ( x e. A /\ x e. B ) <-> ( x e. B /\ x e. A ) )
2		elin 3172	. . 3 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
3		elin 3172	. . 3 |- ( x e. ( B i^i A ) <-> ( x e. B /\ x e. A ) )
4	1, 2, 3	3bitr4i 210	. 2 |- ( x e. ( A i^i B ) <-> x e. ( B i^i A ) )
5	4	eqriv 2082	1 |- ( A i^i B ) = ( B i^i A )

Syntax hints:   /\ wa 102   = wceq 1287   e. wcel 1436   i^i cin 2987

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-in 2994

This theorem is referenced by:  ineq2  3184  dfss1  3193  in12  3200  in32  3201  in13  3202  in31  3203  inss2  3210  sslin  3215  inss  3218  indif1  3233  indifcom  3234  indir  3237  symdif1  3253  dfrab2  3263  disjr  3320  ssdifin0  3351  difdifdirss  3354  uneqdifeqim  3355  diftpsn3  3561  iunin1  3777  iinin1m  3782  riinm  3785  rintm  3800  inex2  3949  onintexmid  4361  resiun1  4699  dmres  4701  rescom  4705  resima2  4713  xpssres  4714  resindm  4721  resdmdfsn  4722  resopab  4723  imadisj  4761  ndmima  4776  intirr  4785  djudisj  4824  imainrect  4842  dmresv  4855  resdmres  4888  funimaexg  5063  fnresdisj  5089  fnimaeq0  5100  resasplitss  5153  f0rn0  5168  fvun2  5334  ressnop0  5441  fvsnun1  5457  fsnunfv  5460  offres  5863  smores3  6012  phplem2  6521  unfiin  6588  xpfi  6590  djuin  6700  fzpreddisj  9415  fseq1p1m1  9438  hashunlem  10108  zfz1isolem1  10141  znnen  11086  bdinex2  11229