Theorem unieqd 3842

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

Syntax hints:   -> wi 4   = wceq 1364   U.cuni 3831

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-uni 3832

This theorem is referenced by:  uniprg  3846  unisng  3848  unisn3  4470  onsucuni2  4588  opswapg  5140  elxp4  5141  elxp5  5142  iotaeq  5211  iotabi  5212  uniabio  5213  funfvdm  5607  funfvdm2  5608  fvun1  5610  fniunfv  5791  funiunfvdm  5792  1stvalg  6175  2ndvalg  6176  fo1st  6190  fo2nd  6191  f1stres  6192  f2ndres  6193  2nd1st  6213  cnvf1olem  6257  brtpos2  6284  dftpos4  6296  tpostpos  6297  recseq  6339  tfrexlem  6367  ixpsnf1o  6770  xpcomco  6860  xpassen  6864  xpdom2  6865  supeq1  7024  supeq2  7027  supeq3  7028  supeq123d  7029  en2other2  7235  dfinfre  8954  hashinfom  10805  hashennn  10807  fsumcnv  11492  fprodcnv  11680  tgval  12784  ptex  12786  lssuni  13722  lspuni0  13783  lss0v  13789  zrhval  13961  zrhvalg  13962  zrhval2  13963  zrhpropd  13970  isbasisg  14063  basis1  14066  baspartn  14069  eltg  14071  ntrfval  14119  ntrval  14129  tgrest  14188  restuni2  14196  lmfval  14211  cnfval  14213  cnpfval  14214  txtopon  14281  txswaphmeolem  14339  peano4nninf  15293