Theorem unieqd 3930

Description: Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)

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

Syntax hints:   -> wi 4   = wceq 1398   U.cuni 3919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-uni 3920

This theorem is referenced by:  uniprg  3934  unisng  3936  unisn3  4571  onsucuni2  4691  opswapg  5254  elxp4  5255  elxp5  5256  iotaeq  5326  iotabi  5327  uniabio  5328  funfvdm  5745  funfvdm2  5746  fvun1  5748  fniunfv  5941  funiunfvdm  5942  1stvalg  6349  2ndvalg  6350  fo1st  6364  fo2nd  6365  f1stres  6366  f2ndres  6367  2nd1st  6387  cnvf1olem  6433  brtpos2  6495  dftpos4  6507  tpostpos  6508  recseq  6550  tfrexlem  6578  ixpsnf1o  6984  xpcomco  7090  xpassen  7094  xpdom2  7095  supeq1  7290  supeq2  7293  supeq3  7294  supeq123d  7295  en2other2  7512  dfinfre  9247  hashinfom  11166  hashennn  11168  fsumcnv  12148  fprodcnv  12336  tgval  13559  ptex  13561  lssuni  14637  lspuni0  14698  lss0v  14704  zrhval  14891  zrhvalg  14892  zrhval2  14893  zrhpropd  14900  isbasisg  15035  basis1  15038  baspartn  15041  eltg  15043  ntrfval  15091  ntrval  15101  tgrest  15160  restuni2  15168  lmfval  15184  cnfval  15185  cnpfval  15186  txtopon  15253  txswaphmeolem  15311  peano4nninf  16910