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

Theorem iuneq1 4566
Description: Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998.)
Assertion
Ref Expression
iuneq1 (𝐴 = 𝐵 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem iuneq1
StepHypRef Expression
1 iunss1 4564 . . 3 (𝐴𝐵 𝑥𝐴 𝐶 𝑥𝐵 𝐶)
2 iunss1 4564 . . 3 (𝐵𝐴 𝑥𝐵 𝐶 𝑥𝐴 𝐶)
31, 2anim12i 589 . 2 ((𝐴𝐵𝐵𝐴) → ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶 𝑥𝐵 𝐶 𝑥𝐴 𝐶))
4 eqss 3651 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3651 . 2 ( 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶 ↔ ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶 𝑥𝐵 𝐶 𝑥𝐴 𝐶))
63, 4, 53imtr4i 281 1 (𝐴 = 𝐵 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wss 3607   ciun 4552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-v 3233  df-in 3614  df-ss 3621  df-iun 4554
This theorem is referenced by:  iuneq1d  4577  iinvdif  4624  iunxprg  4639  iununi  4642  iunsuc  5845  funopsn  6453  funiunfv  6546  onfununi  7483  iunfi  8295  rankuni2b  8754  pwsdompw  9064  ackbij1lem7  9086  r1om  9104  fictb  9105  cfsmolem  9130  ituniiun  9282  domtriomlem  9302  domtriom  9303  inar1  9635  fsum2d  14546  fsumiun  14597  ackbijnn  14604  fprod2d  14755  prmreclem5  15671  lpival  19293  fiuncmp  21255  ovolfiniun  23315  ovoliunnul  23321  finiunmbl  23358  volfiniun  23361  voliunlem1  23364  iuninc  29505  ofpreima2  29594  esum2dlem  30282  sigaclfu2  30312  sigapildsyslem  30352  fiunelros  30365  bnj548  31093  bnj554  31095  bnj594  31108  trpredlem1  31851  trpredtr  31854  trpredmintr  31855  trpredrec  31862  neibastop2lem  32480  istotbnd3  33700  0totbnd  33702  sstotbnd2  33703  sstotbnd  33704  sstotbnd3  33705  totbndbnd  33718  prdstotbnd  33723  cntotbnd  33725  heibor  33750  dfrcl4  38285  iunrelexp0  38311  comptiunov2i  38315  corclrcl  38316  cotrcltrcl  38334  trclfvdecomr  38337  dfrtrcl4  38347  corcltrcl  38348  cotrclrcl  38351  fiiuncl  39548  iuneq1i  39573  sge0iunmptlemfi  40948  caragenfiiuncl  41050  carageniuncllem1  41056  ovnsubadd2lem  41180
  Copyright terms: Public domain W3C validator