Theorem unieqd 2512

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 2510	. 2 |- (A = B -> U.A = U.B)
3	1, 2	syl 10	1 |- (ph -> U.A = U.B)

Syntax hints:   -> wi 3   = wceq 956  U.cuni 2503

This theorem is referenced by:  uniprg 2516  unisng 2518  unisn2 2875  unisn3 2876  ordunisuc 3089  orduniss2 3090  elxp4 3453  elxp5 3454  fvprc 3721  fveq1 3723  fveq2 3724  fvres 3734  funfv 3770  funfv2 3771  fvopabn 3786  fvopab5 3793  fniunfv 3865  tz7.44-3 3930  rdgeq1 3934  rdgeq2 3935  rdglem2 3938  rdglimt 3948  rdglim2 3949  1stval 4081  2ndval 4082  fo1st 4091  fo2nd 4092  f1stres 4093  f2ndres 4094  1st2val 4095  2nd2val 4096  oaabs 4252  xpcomen 4439  xpassen 4441  xpdom2 4442  xpmapenlem2 4497  xpmapenlem4 4499  xpmapenlem5 4500  mapunen 4502  unifiOLD 4557  supeq1 4575  rankuni 4698  aceq6a 4741  kmlem9 4773  kmlem11 4775  kmlem12 4776  zorn2lem1 4788  zorn2 4796  subvalt 5357  divval 5704  dfinfmr 6067  infmsup 6068  supxrre 6083  flvalt 6225  revalt 6755  imvalt 6756  sumeq1 6982  sumeq2 6985  dffsum 6998  dfisum 7191  isumvalt 7192  isumnul 7203  acdc3lem 7486  acdc3 7487  acdc2lem1 7488  acdc2 7490  acdc5lem1 7491  acdc5 7493  acdclem 7494  acdc 7495  xpnnen 7499  isbasisg 7611  basis1t 7614  tgvalt 7616  eltgt 7618  ntrfval 7667  ntrval 7676  cncnplem4 7777  bcth 8032  grpidval 8058  grpinvfval 8066  grpinvval 8067  addinv 8128  isps 8645  spwval2 8653  spwval 8659  spwpr4OLD 8663  spwpr4aOLD 8664  pjmvalt 9238  pjvalt 9239  adjvalt 9814  adjval2t 9815  cnlnadjlem4 10003  nmopadjle 10021  cdj3lem2 10362

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-uni 2504

Copyright terms: Public domain