Theorem incom 3401

Description: Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
incom	⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)

Proof of Theorem incom

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ancom 266	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))
2		elin 3392	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
3		elin 3392	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))
4	1, 2, 3	3bitr4i 212	. 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ 𝑥 ∈ (𝐵 ∩ 𝐴))
5	4	eqriv 2228	1 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)

Syntax hints:   ∧ wa 104   = wceq 1398   ∈ wcel 2202   ∩ cin 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-in 3207

This theorem is referenced by:  ineq2  3404  dfss1  3413  in12  3420  in32  3421  in13  3422  in31  3423  inss2  3430  sslin  3435  inss  3439  indif1  3454  indifcom  3455  indir  3458  symdif1  3474  dfrab2  3484  0in  3532  disjr  3546  ssdifin0  3578  difdifdirss  3581  uneqdifeqim  3582  diftpsn3  3819  iunin1  4040  iinin1m  4045  riinm  4048  rintm  4068  inex2  4229  onintexmid  4677  resiun1  5038  dmres  5040  rescom  5044  resima2  5053  xpssres  5054  resindm  5061  resdmdfsn  5062  resopab  5063  imadisj  5105  ndmima  5120  intirr  5130  djudisj  5171  imainrect  5189  dmresv  5202  resdmres  5235  funimaexg  5421  fnresdisj  5449  fnimaeq0  5461  resasplitss  5524  f0rn0  5540  fvun2  5722  ressnop0  5843  fvsnun1  5859  fsnunfv  5863  offres  6306  smores3  6502  phplem2  7082  unfiin  7161  xpfi  7167  endjusym  7338  djucomen  7474  fzpreddisj  10351  fseq1p1m1  10374  hashunlem  11113  zfz1isolem1  11150  fprodsplit  12221  znnen  13082  setsfun  13180  setsfun0  13181  setsslid  13196  ressressg  13221  restin  14970  metreslem  15174  perfectlem2  15797  bdinex2  16599  gfsump1  16798