Theorem unieqd 2507

Description: Deduction of equality of two class unions.

Hypothesis

Ref	Expression
unieqd.1	|- (ph -> A = B)

Assertion

Ref	Expression
unieqd	|- (ph -> U.A = U.B)

Proof of Theorem unieqd

Step	Hyp	Ref	Expression
1		unieqd.1	. 2 |- (ph -> A = B)
2		unieq 2505	. 2 |- (A = B -> U.A = U.B)
3	1, 2	syl 10	1 |- (ph -> U.A = U.B)

Syntax hints:   -> wi 3   = wceq 954  U.cuni 2498

This theorem is referenced by:  uniprg 2511  unisng 2513  unisn2 2870  unisn3 2871  ordunisuc 3084  orduniss2 3085  elxp4 3445  elxp5 3446  fvprc 3712  fveq1 3714  fveq2 3715  fvres 3725  funfv 3761  funfv2 3762  fvopabn 3777  fvopab5 3784  fniunfv 3856  tz7.44-3 3921  rdgeq1 3925  rdgeq2 3926  rdglem2 3929  rdglimt 3939  rdglim2 3940  1stval 4071  2ndval 4072  fo1st 4081  fo2nd 4082  f1stres 4083  f2ndres 4084  1st2val 4085  2nd2val 4086  oaabs 4242  xpcomen 4425  xpassen 4427  xpdom2 4428  xpmapenlem2 4483  xpmapenlem4 4485  xpmapenlem5 4486  mapunen 4488  unifi 4538  supeq1 4555  rankuni 4678  aceq6a 4721  kmlem9 4753  kmlem11 4755  kmlem12 4756  zorn2lem1 4768  zorn2 4776  subvalt 5337  divval 5681  dfinfmr 6022  infmsup 6023  supxrre 6038  flvalt 6181  revalt 6694  imvalt 6695  sumeq1 6928  sumeq2 6931  dffsum 6944  dfisum 7135  isumvalt 7136  isumnul 7146  acdc3lem 7436  acdc3 7437  acdc2lem1 7438  acdc2 7440  acdc5lem1 7441  acdc5 7443  acdclem 7444  acdc 7445  xpnnen 7449  isbasisg 7561  basis1t 7564  tgvalt 7566  eltgt 7568  ntrfval 7617  ntrval 7626  cncnplem4 7727  bcth 7982  grpidval 8008  grpinvfval 8016  grpinvval 8017  addinv 8080  isps 8588  spwval2 8595  spwval 8600  pjmvalt 9176  pjvalt 9177  adjvalt 9754  adjval2t 9755  cnlnadjlem4 9941  nmopadjle 9959  cdj3lem2 10296

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-uni 2499

Copyright terms: Public domain