MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  inass Structured version   Visualization version   GIF version

Theorem inass 4220
Description: Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.)
Assertion
Ref Expression
inass ((𝐴𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵𝐶))

Proof of Theorem inass
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 anass 467 . . . 4 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
2 elin 3962 . . . . 5 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
32anbi2i 621 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∧ (𝑥𝐵𝑥𝐶)))
41, 3bitr4i 277 . . 3 (((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
5 elin 3962 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
65anbi1i 622 . . 3 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶))
7 elin 3962 . . 3 (𝑥 ∈ (𝐴 ∩ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
84, 6, 73bitr4i 302 . 2 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑥𝐶) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵𝐶)))
98ineqri 4204 1 ((𝐴𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 394   = wceq 1533  wcel 2098  cin 3945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-in 3953
This theorem is referenced by:  in12  4221  in32  4222  in4  4226  indif2  4271  difun1  4290  dfrab3ss  4314  dfif4  4547  resres  6001  inres  6006  imainrect  6191  cnvrescnv  6205  predidm  6338  onfr  6414  fresaun  6772  fresaunres2  6773  fimacnvinrn2  7085  epfrs  9770  incexclem  15835  sadeq  16467  smuval2  16477  smumul  16488  ressinbas  17254  ressress  17257  resscatc  18126  sylow2a  19612  ablfac1eu  20068  ressmplbas2  22026  restco  23151  restopnb  23162  kgeni  23524  hausdiag  23632  fclsrest  24011  clsocv  25261  itg2cnlem2  25775  rplogsum  27548  chjassi  31411  pjoml2i  31510  cmcmlem  31516  cmbr3i  31525  fh1  31543  fh2  31544  pj3lem1  32131  dmdbr5  32233  mdslmd3i  32257  mdexchi  32260  atabsi  32326  dmdbr6ati  32348  prsss  33687  inelcarsg  34101  carsgclctunlem1  34107  msrid  35325  redundss3  38274  refrelsredund4  38278  osumcllem9N  39611  dihmeetbclemN  40951  dihmeetlem11N  40964  inabs3  44594  uzinico2  45117  caragenuncllem  46070  restclsseplem  48185
  Copyright terms: Public domain W3C validator