Theorem incom 3421

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

Syntax hints:   ∧ wa 104   = wceq 1402   ∈ wcel 2209   ∩ cin 3219

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226

This theorem is referenced by:  ineqcom  3422  ineqcomi  3423  ineq2  3426  dfss1  3435  in12  3442  in32  3443  in13  3444  in31  3445  inss2  3452  sslin  3457  inss  3461  indif1  3476  indifcom  3477  indir  3480  symdif1  3496  dfrab2  3508  0in  3558  disjr  3573  ssdifin0  3606  difdifdirss  3609  uneqdifeqim  3610  diftpsn3  3851  iunin1  4072  iinin1m  4077  riinm  4080  rintm  4100  inex2  4263  onintexmid  4715  resiun1  5077  dmres  5079  rescom  5083  resima2  5092  xpssres  5093  resindm  5100  resdmdfsn  5101  resopab  5102  imadisj  5144  ndmima  5159  intirr  5169  djudisj  5210  imainrect  5228  dmresv  5241  resdmres  5274  funimaexg  5460  fnresdisj  5488  fnimaeq0  5500  resasplitss  5564  fresaunres1disj  5566  f0rn0  5582  fvun2  5764  ressnop0  5887  fvsnun1  5903  fsnunfv  5907  offres  6358  smores3  6554  phplem2  7144  unfiin  7223  xpfi  7229  endjusym  7426  djucomen  7562  fzpreddisj  10456  fseq1p1m1  10479  hashunlem  11222  hashfibclem  11260  zfz1isolem1  11270  fprodsplit  12342  ballotfilemfval0  13213  znnen  13267  setsfun  13365  setsfun0  13366  setsslid  13381  ressressg  13406  restin  15200  metreslem  15404  perfectlem2  16028  bdinex2  16840