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

Theorem iuneq1 4722
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 4720 . . 3 (𝐴𝐵 𝑥𝐴 𝐶 𝑥𝐵 𝐶)
2 iunss1 4720 . . 3 (𝐵𝐴 𝑥𝐵 𝐶 𝑥𝐴 𝐶)
31, 2anim12i 602 . 2 ((𝐴𝐵𝐵𝐴) → ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶 𝑥𝐵 𝐶 𝑥𝐴 𝐶))
4 eqss 3810 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3810 . 2 ( 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶 ↔ ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶 𝑥𝐵 𝐶 𝑥𝐴 𝐶))
63, 4, 53imtr4i 283 1 (𝐴 = 𝐵 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wss 3766   ciun 4708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ral 3100  df-rex 3101  df-v 3392  df-in 3773  df-ss 3780  df-iun 4710
This theorem is referenced by:  iuneq1d  4733  iinvdif  4780  iunxprg  4795  iununi  4798  iunsuc  6017  funopsn  6634  funiunfv  6727  onfununi  7671  iunfi  8490  rankuni2b  8960  pwsdompw  9308  ackbij1lem7  9330  r1om  9348  fictb  9349  cfsmolem  9374  ituniiun  9526  domtriomlem  9546  domtriom  9547  inar1  9879  fsum2d  14721  fsumiun  14771  ackbijnn  14778  fprod2d  14928  prmreclem5  15837  lpival  19450  fiuncmp  21417  ovolfiniun  23478  ovoliunnul  23484  finiunmbl  23521  volfiniun  23524  voliunlem1  23527  iuninc  29701  ofpreima2  29790  esum2dlem  30476  sigaclfu2  30506  sigapildsyslem  30546  fiunelros  30559  bnj548  31287  bnj554  31289  bnj594  31302  trpredlem1  32044  trpredtr  32047  trpredmintr  32048  trpredrec  32055  neibastop2lem  32673  istotbnd3  33878  0totbnd  33880  sstotbnd2  33881  sstotbnd  33882  sstotbnd3  33883  totbndbnd  33896  prdstotbnd  33901  cntotbnd  33903  heibor  33928  dfrcl4  38465  iunrelexp0  38491  comptiunov2i  38495  corclrcl  38496  cotrcltrcl  38514  trclfvdecomr  38517  dfrtrcl4  38527  corcltrcl  38528  cotrclrcl  38531  fiiuncl  39724  iuneq1i  39749  sge0iunmptlemfi  41106  caragenfiiuncl  41208  carageniuncllem1  41214  ovnsubadd2lem  41338
  Copyright terms: Public domain W3C validator