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  5834  fvsnun1  5850  fsnunfv  5854  offres  6296  smores3  6458  phplem2  7038  unfiin  7117  xpfi  7123  endjusym  7294  djucomen  7430  fzpreddisj  10305  fseq1p1m1  10328  hashunlem  11066  zfz1isolem1  11103  fprodsplit  12157  znnen  13018  setsfun  13116  setsfun0  13117  setsslid  13132  ressressg  13157  restin  14899  metreslem  15103  perfectlem2  15723  bdinex2  16495