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

Theorem iuneq2 4928
Description: Equality theorem for indexed union. (Contributed by NM, 22-Oct-2003.)
Assertion
Ref Expression
iuneq2 (∀𝑥𝐴 𝐵 = 𝐶 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)

Proof of Theorem iuneq2
StepHypRef Expression
1 ss2iun 4927 . . 3 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 𝑥𝐴 𝐶)
2 ss2iun 4927 . . 3 (∀𝑥𝐴 𝐶𝐵 𝑥𝐴 𝐶 𝑥𝐴 𝐵)
31, 2anim12i 616 . 2 ((∀𝑥𝐴 𝐵𝐶 ∧ ∀𝑥𝐴 𝐶𝐵) → ( 𝑥𝐴 𝐵 𝑥𝐴 𝐶 𝑥𝐴 𝐶 𝑥𝐴 𝐵))
4 eqss 3921 . . . 4 (𝐵 = 𝐶 ↔ (𝐵𝐶𝐶𝐵))
54ralbii 3088 . . 3 (∀𝑥𝐴 𝐵 = 𝐶 ↔ ∀𝑥𝐴 (𝐵𝐶𝐶𝐵))
6 r19.26 3092 . . 3 (∀𝑥𝐴 (𝐵𝐶𝐶𝐵) ↔ (∀𝑥𝐴 𝐵𝐶 ∧ ∀𝑥𝐴 𝐶𝐵))
75, 6bitri 278 . 2 (∀𝑥𝐴 𝐵 = 𝐶 ↔ (∀𝑥𝐴 𝐵𝐶 ∧ ∀𝑥𝐴 𝐶𝐵))
8 eqss 3921 . 2 ( 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶 ↔ ( 𝑥𝐴 𝐵 𝑥𝐴 𝐶 𝑥𝐴 𝐶 𝑥𝐴 𝐵))
93, 7, 83imtr4i 295 1 (∀𝑥𝐴 𝐵 = 𝐶 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1543  wral 3061  wss 3871   ciun 4909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-v 3415  df-in 3878  df-ss 3888  df-iun 4911
This theorem is referenced by:  iuneq2i  4930  iuneq2dv  4933  iunxdif3  5008  oa0r  8270  om0r  8271  om1r  8276  oe1m  8278  oaass  8294  oarec  8295  omass  8313  oeoalem  8329  oeoelem  8331  cardiun  9603  kmlem11  9779  iuncld  21947  comppfsc  22434  istotbnd3  35671  sstotbnd  35675  heibor  35721  iuneq12f  36063  cnvtrclfv  41017  iuneq2df  42275
  Copyright terms: Public domain W3C validator