Theorem incom 3158

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

Syntax hints:   /\ wa 102   = wceq 1284   e. wcel 1433   i^i cin 2972

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 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-in 2979

This theorem is referenced by:  ineq2  3161  dfss1  3170  in12  3177  in32  3178  in13  3179  in31  3180  inss2  3187  sslin  3192  inss  3195  indif1  3209  indifcom  3210  indir  3213  symdif1  3229  dfrab2  3239  disjr  3293  ssdifin0  3324  difdifdirss  3327  uneqdifeqim  3328  diftpsn3  3527  iunin1  3742  iinin1m  3747  riinm  3750  rintm  3765  inex2  3913  onintexmid  4315  resiun1  4648  dmres  4650  rescom  4654  resima2  4662  xpssres  4663  resindm  4670  resdmdfsn  4671  resopab  4672  imadisj  4707  ndmima  4722  intirr  4731  djudisj  4770  imainrect  4786  dmresv  4799  resdmres  4832  funimaexg  5003  fnresdisj  5029  fnimaeq0  5040  resasplitss  5089  fvun2  5261  ressnop0  5365  fvsnun1  5381  fsnunfv  5384  offres  5782  smores3  5931  phplem2  6339  fzpreddisj  9088  fseq1p1m1  9111  bdinex2  10691