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

Theorem iuneq1 4840
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 4838 . . 3 (𝐴𝐵 𝑥𝐴 𝐶 𝑥𝐵 𝐶)
2 iunss1 4838 . . 3 (𝐵𝐴 𝑥𝐵 𝐶 𝑥𝐴 𝐶)
31, 2anim12i 612 . 2 ((𝐴𝐵𝐵𝐴) → ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶 𝑥𝐵 𝐶 𝑥𝐴 𝐶))
4 eqss 3904 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3904 . 2 ( 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶 ↔ ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶 𝑥𝐵 𝐶 𝑥𝐴 𝐶))
63, 4, 53imtr4i 293 1 (𝐴 = 𝐵 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1522  wss 3859   ciun 4825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-v 3439  df-in 3866  df-ss 3874  df-iun 4827
This theorem is referenced by:  iuneq1d  4851  iinvdif  4901  iunxprg  4917  iununi  4920  iunsuc  6148  funopsn  6773  funiunfv  6872  onfununi  7830  iunfi  8658  rankuni2b  9128  pwsdompw  9472  ackbij1lem7  9494  r1om  9512  fictb  9513  cfsmolem  9538  ituniiun  9690  domtriomlem  9710  domtriom  9711  inar1  10043  fsum2d  14959  fsumiun  15009  ackbijnn  15016  fprod2d  15168  prmreclem5  16085  lpival  19707  fiuncmp  21696  ovolfiniun  23785  ovoliunnul  23791  finiunmbl  23828  volfiniun  23831  voliunlem1  23834  iuninc  30002  ofpreima2  30101  esum2dlem  30968  sigaclfu2  30997  sigapildsyslem  31037  fiunelros  31050  bnj548  31785  bnj554  31787  bnj594  31800  trpredlem1  32675  trpredtr  32678  trpredmintr  32679  trpredrec  32686  neibastop2lem  33317  istotbnd3  34581  0totbnd  34583  sstotbnd2  34584  sstotbnd  34585  sstotbnd3  34586  totbndbnd  34599  prdstotbnd  34604  cntotbnd  34606  heibor  34631  dfrcl4  39506  iunrelexp0  39532  comptiunov2i  39536  corclrcl  39537  cotrcltrcl  39555  trclfvdecomr  39558  dfrtrcl4  39568  corcltrcl  39569  cotrclrcl  39572  fiiuncl  40866  iuneq1i  40889  sge0iunmptlemfi  42237  caragenfiiuncl  42339  carageniuncllem1  42345  ovnsubadd2lem  42469
  Copyright terms: Public domain W3C validator