Theorem incom 3327

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

Syntax hints:   ∧ wa 104   = wceq 1353   ∈ wcel 2148   ∩ cin 3128

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-in 3135

This theorem is referenced by:  ineq2  3330  dfss1  3339  in12  3346  in32  3347  in13  3348  in31  3349  inss2  3356  sslin  3361  inss  3365  indif1  3380  indifcom  3381  indir  3384  symdif1  3400  dfrab2  3410  0in  3458  disjr  3472  ssdifin0  3504  difdifdirss  3507  uneqdifeqim  3508  diftpsn3  3733  iunin1  3951  iinin1m  3956  riinm  3959  rintm  3979  inex2  4138  onintexmid  4572  resiun1  4926  dmres  4928  rescom  4932  resima2  4941  xpssres  4942  resindm  4949  resdmdfsn  4950  resopab  4951  imadisj  4990  ndmima  5005  intirr  5015  djudisj  5056  imainrect  5074  dmresv  5087  resdmres  5120  funimaexg  5300  fnresdisj  5326  fnimaeq0  5337  resasplitss  5395  f0rn0  5410  fvun2  5583  ressnop0  5697  fvsnun1  5713  fsnunfv  5717  offres  6135  smores3  6293  phplem2  6852  unfiin  6924  xpfi  6928  endjusym  7094  djucomen  7214  fzpreddisj  10070  fseq1p1m1  10093  hashunlem  10783  zfz1isolem1  10819  fprodsplit  11604  znnen  12398  setsfun  12496  setsfun0  12497  setsslid  12512  ressressg  12533  restin  13646  metreslem  13850  bdinex2  14622