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

Theorem incom 3126
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 253 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵𝑥𝐴))
2 elin 3123 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
3 elin 3123 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
41, 2, 33bitr4i 201 . 2 (𝑥 ∈ (𝐴𝐵) ↔ 𝑥 ∈ (𝐵𝐴))
54eqriv 2037 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff set class
Syntax hints:  wa 97   = wceq 1243  wcel 1393  cin 2913
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2556  df-in 2921
This theorem is referenced by:  ineq2  3129  dfss1  3138  in12  3145  in32  3146  in13  3147  in31  3148  inss2  3155  sslin  3160  inss  3163  indif1  3179  indifcom  3180  indir  3183  symdif1  3199  dfrab2  3209  disjr  3266  ssdifin0  3301  difdifdirss  3304  uneqdifeqim  3305  diftpsn3  3502  iunin1  3718  iinin1m  3723  riinm  3726  rintm  3741  inex2  3889  onintexmid  4291  resiun1  4617  dmres  4619  rescom  4623  resima2  4631  xpssres  4632  resopab  4639  imadisj  4674  ndmima  4689  intirr  4698  djudisj  4737  imainrect  4753  dmresv  4766  resdmres  4799  funimaexg  4970  fnresdisj  4996  fnimaeq0  5007  resasplitss  5056  fvun2  5227  ressnop0  5331  fvsnun1  5347  fsnunfv  5350  offres  5749  smores3  5895  phplem2  6303  fzpreddisj  8900  fseq1p1m1  8923  bdinex2  9893
  Copyright terms: Public domain W3C validator