Theorem incom 3397

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 3388	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
3		elin 3388	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))
4	1, 2, 3	3bitr4i 212	. 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ 𝑥 ∈ (𝐵 ∩ 𝐴))
5	4	eqriv 2226	1 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)

Syntax hints:   ∧ wa 104   = wceq 1395   ∈ wcel 2200   ∩ cin 3197

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-in 3204

This theorem is referenced by:  ineq2  3400  dfss1  3409  in12  3416  in32  3417  in13  3418  in31  3419  inss2  3426  sslin  3431  inss  3435  indif1  3450  indifcom  3451  indir  3454  symdif1  3470  dfrab2  3480  0in  3528  disjr  3542  ssdifin0  3574  difdifdirss  3577  uneqdifeqim  3578  diftpsn3  3812  iunin1  4033  iinin1m  4038  riinm  4041  rintm  4061  inex2  4222  onintexmid  4669  resiun1  5030  dmres  5032  rescom  5036  resima2  5045  xpssres  5046  resindm  5053  resdmdfsn  5054  resopab  5055  imadisj  5096  ndmima  5111  intirr  5121  djudisj  5162  imainrect  5180  dmresv  5193  resdmres  5226  funimaexg  5411  fnresdisj  5439  fnimaeq0  5451  resasplitss  5513  f0rn0  5528  fvun2  5709  ressnop0  5830  fvsnun1  5846  fsnunfv  5850  offres  6292  smores3  6454  phplem2  7034  unfiin  7111  xpfi  7117  endjusym  7286  djucomen  7421  fzpreddisj  10296  fseq1p1m1  10319  hashunlem  11057  zfz1isolem1  11094  fprodsplit  12148  znnen  13009  setsfun  13107  setsfun0  13108  setsslid  13123  ressressg  13148  restin  14890  metreslem  15094  perfectlem2  15714  bdinex2  16431