Theorem incom 3373

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

Syntax hints:   ∧ wa 104   = wceq 1373   ∈ wcel 2178   ∩ cin 3173

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-in 3180

This theorem is referenced by:  ineq2  3376  dfss1  3385  in12  3392  in32  3393  in13  3394  in31  3395  inss2  3402  sslin  3407  inss  3411  indif1  3426  indifcom  3427  indir  3430  symdif1  3446  dfrab2  3456  0in  3504  disjr  3518  ssdifin0  3550  difdifdirss  3553  uneqdifeqim  3554  diftpsn3  3785  iunin1  4006  iinin1m  4011  riinm  4014  rintm  4034  inex2  4195  onintexmid  4639  resiun1  4997  dmres  4999  rescom  5003  resima2  5012  xpssres  5013  resindm  5020  resdmdfsn  5021  resopab  5022  imadisj  5063  ndmima  5078  intirr  5088  djudisj  5129  imainrect  5147  dmresv  5160  resdmres  5193  funimaexg  5377  fnresdisj  5405  fnimaeq0  5417  resasplitss  5477  f0rn0  5492  fvun2  5669  ressnop0  5788  fvsnun1  5804  fsnunfv  5808  offres  6243  smores3  6402  phplem2  6975  unfiin  7049  xpfi  7055  endjusym  7224  djucomen  7359  fzpreddisj  10228  fseq1p1m1  10251  hashunlem  10986  zfz1isolem1  11022  fprodsplit  12023  znnen  12884  setsfun  12982  setsfun0  12983  setsslid  12998  ressressg  13022  restin  14763  metreslem  14967  perfectlem2  15587  bdinex2  16035