ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  incom GIF version

Theorem incom 3157
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.
StepHypRef Expression
1 ancom 257 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵𝑥𝐴))
2 elin 3154 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
3 elin 3154 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
41, 2, 33bitr4i 205 . 2 (𝑥 ∈ (𝐴𝐵) ↔ 𝑥 ∈ (𝐵𝐴))
54eqriv 2053 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff set class
Syntax hints:  wa 101   = wceq 1259  wcel 1409  cin 2944
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-in 2952
This theorem is referenced by:  ineq2  3160  dfss1  3169  in12  3176  in32  3177  in13  3178  in31  3179  inss2  3186  sslin  3191  inss  3194  indif1  3210  indifcom  3211  indir  3214  symdif1  3230  dfrab2  3240  disjr  3297  ssdifin0  3332  difdifdirss  3335  uneqdifeqim  3336  diftpsn3  3533  iunin1  3749  iinin1m  3754  riinm  3757  rintm  3772  inex2  3920  onintexmid  4325  resiun1  4658  dmres  4660  rescom  4664  resima2  4672  xpssres  4673  resopab  4680  imadisj  4715  ndmima  4730  intirr  4739  djudisj  4778  imainrect  4794  dmresv  4807  resdmres  4840  funimaexg  5011  fnresdisj  5037  fnimaeq0  5048  resasplitss  5097  fvun2  5268  ressnop0  5372  fvsnun1  5388  fsnunfv  5391  offres  5790  smores3  5939  phplem2  6347  fzpreddisj  9035  fseq1p1m1  9058  bdinex2  10407
  Copyright terms: Public domain W3C validator