Theorem incom 3234

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

Syntax hints:   ∧ wa 103   = wceq 1314   ∈ wcel 1463   ∩ cin 3036

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-v 2659  df-in 3043

This theorem is referenced by:  ineq2  3237  dfss1  3246  in12  3253  in32  3254  in13  3255  in31  3256  inss2  3263  sslin  3268  inss  3272  indif1  3287  indifcom  3288  indir  3291  symdif1  3307  dfrab2  3317  0in  3364  disjr  3378  ssdifin0  3410  difdifdirss  3413  uneqdifeqim  3414  diftpsn3  3627  iunin1  3843  iinin1m  3848  riinm  3851  rintm  3871  inex2  4023  onintexmid  4447  resiun1  4796  dmres  4798  rescom  4802  resima2  4811  xpssres  4812  resindm  4819  resdmdfsn  4820  resopab  4821  imadisj  4859  ndmima  4874  intirr  4883  djudisj  4924  imainrect  4942  dmresv  4955  resdmres  4988  funimaexg  5165  fnresdisj  5191  fnimaeq0  5202  resasplitss  5260  f0rn0  5275  fvun2  5442  ressnop0  5555  fvsnun1  5571  fsnunfv  5575  offres  5987  smores3  6144  phplem2  6700  unfiin  6767  xpfi  6771  endjusym  6933  djucomen  7020  fzpreddisj  9744  fseq1p1m1  9767  hashunlem  10443  zfz1isolem1  10476  znnen  11756  setsfun  11837  setsfun0  11838  setsslid  11852  restin  12188  metreslem  12369  bdinex2  12790