Theorem incom 3399

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

Syntax hints:   ∧ wa 104   = wceq 1397   ∈ wcel 2202   ∩ cin 3199

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-in 3206

This theorem is referenced by:  ineq2  3402  dfss1  3411  in12  3418  in32  3419  in13  3420  in31  3421  inss2  3428  sslin  3433  inss  3437  indif1  3452  indifcom  3453  indir  3456  symdif1  3472  dfrab2  3482  0in  3530  disjr  3544  ssdifin0  3576  difdifdirss  3579  uneqdifeqim  3580  diftpsn3  3814  iunin1  4035  iinin1m  4040  riinm  4043  rintm  4063  inex2  4224  onintexmid  4671  resiun1  5032  dmres  5034  rescom  5038  resima2  5047  xpssres  5048  resindm  5055  resdmdfsn  5056  resopab  5057  imadisj  5098  ndmima  5113  intirr  5123  djudisj  5164  imainrect  5182  dmresv  5195  resdmres  5228  funimaexg  5414  fnresdisj  5442  fnimaeq0  5454  resasplitss  5516  f0rn0  5531  fvun2  5713  ressnop0  5835  fvsnun1  5851  fsnunfv  5855  offres  6297  smores3  6459  phplem2  7039  unfiin  7118  xpfi  7124  endjusym  7295  djucomen  7431  fzpreddisj  10306  fseq1p1m1  10329  hashunlem  11068  zfz1isolem1  11105  fprodsplit  12176  znnen  13037  setsfun  13135  setsfun0  13136  setsslid  13151  ressressg  13176  restin  14919  metreslem  15123  perfectlem2  15743  bdinex2  16546  gfsump1  16738