Theorem incom 3364

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

Syntax hints:   ∧ wa 104   = wceq 1372   ∈ wcel 2175   ∩ cin 3164

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-in 3171

This theorem is referenced by:  ineq2  3367  dfss1  3376  in12  3383  in32  3384  in13  3385  in31  3386  inss2  3393  sslin  3398  inss  3402  indif1  3417  indifcom  3418  indir  3421  symdif1  3437  dfrab2  3447  0in  3495  disjr  3509  ssdifin0  3541  difdifdirss  3544  uneqdifeqim  3545  diftpsn3  3773  iunin1  3991  iinin1m  3996  riinm  3999  rintm  4019  inex2  4178  onintexmid  4620  resiun1  4977  dmres  4979  rescom  4983  resima2  4992  xpssres  4993  resindm  5000  resdmdfsn  5001  resopab  5002  imadisj  5043  ndmima  5058  intirr  5068  djudisj  5109  imainrect  5127  dmresv  5140  resdmres  5173  funimaexg  5357  fnresdisj  5385  fnimaeq0  5396  resasplitss  5454  f0rn0  5469  fvun2  5645  ressnop0  5764  fvsnun1  5780  fsnunfv  5784  offres  6219  smores3  6378  phplem2  6949  unfiin  7022  xpfi  7028  endjusym  7197  djucomen  7327  fzpreddisj  10192  fseq1p1m1  10215  hashunlem  10947  zfz1isolem1  10983  fprodsplit  11879  znnen  12740  setsfun  12838  setsfun0  12839  setsslid  12854  ressressg  12878  restin  14619  metreslem  14823  perfectlem2  15443  bdinex2  15798