Theorem unieqd 3946

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   U.cuni 3935

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3936

This theorem is used by:  uniprg  3950  unisng  3952  unisn3  4593  onsucuni2  4713  opswapg  5277  elxp4  5278  elxp5  5279  iotaeq  5349  iotabi  5350  uniabio  5351  funfvdm  5769  funfvdm2  5770  fvun1  5772  fniunfv  5971  funiunfvdm  5972  1stvalg  6380  2ndvalg  6381  fo1st  6395  fo2nd  6396  f1stres  6397  f2ndres  6398  2nd1st  6418  cnvf1olem  6464  brtpos2  6527  dftpos4  6539  tpostpos  6540  recseq  6582  tfrexlem  6610  ixpsnf1o  7024  xpcomco  7130  xpassen  7134  xpdom2  7135  supeq1  7332  supeq2  7335  supeq3  7336  supeq123d  7337  en2other2  7554  dfinfre  9294  hashinfom  11238  hashennn  11240  fsumcnv  12228  fprodcnv  12416  tgval  13674  ptex  13676  gsumcom2fi  14274  lssuni  14808  lspuni0  14869  lss0v  14875  zrhval  15060  zrhvalg  15061  zrhval2  15062  zrhpropd  15069  isbasisg  15287  basis1  15290  baspartn  15293  eltg  15295  ntrfval  15343  ntrval  15353  tgrest  15412  restuni2  15420  lmfval  15436  cnfval  15437  cnpfval  15438  txtopon  15505  txswaphmeolem  15563  peano4nninf  17272