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

Theorem incom 3106
Description: Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
incom (AB) = (BA)

Proof of Theorem incom
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 ancom 253 . . 3 ((x A x B) ↔ (x B x A))
2 elin 3103 . . 3 (x (AB) ↔ (x A x B))
3 elin 3103 . . 3 (x (BA) ↔ (x B x A))
41, 2, 33bitr4i 201 . 2 (x (AB) ↔ x (BA))
54eqriv 2019 1 (AB) = (BA)
Colors of variables: wff set class
Syntax hints:   wa 97   = wceq 1228   wcel 1374  cin 2893
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 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-v 2537  df-in 2901
This theorem is referenced by:  ineq2  3109  dfss1  3118  in12  3125  in32  3126  in13  3127  in31  3128  inss2  3135  sslin  3140  inss  3143  indif1  3159  indifcom  3160  indir  3163  symdif1  3179  dfrab2  3189  disjr  3246  ssdifin0  3281  difdifdirss  3284  uneqdifeqim  3285  diftpsn3  3479  iunin1  3695  iinin1m  3700  riinm  3703  rintm  3718  inex2  3866  resiun1  4557  dmres  4559  rescom  4563  resima2  4571  xpssres  4572  resopab  4579  imadisj  4614  ndmima  4629  intirr  4638  djudisj  4677  imainrect  4693  dmresv  4706  resdmres  4739  funimaexg  4909  fnresdisj  4935  fnimaeq0  4946  resasplitss  4994  fvun2  5165  ressnop0  5269  fvsnun1  5285  fsnunfv  5288  offres  5685  smores3  5830  bdinex2  7270
  Copyright terms: Public domain W3C validator