Theorem unieqd 3847

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 3845	. 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 3836

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 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-uni 3837

This theorem is referenced by:  uniprg  3851  unisng  3853  unisn3  4477  onsucuni2  4597  opswapg  5153  elxp4  5154  elxp5  5155  iotaeq  5224  iotabi  5225  uniabio  5226  funfvdm  5621  funfvdm2  5622  fvun1  5624  fniunfv  5806  funiunfvdm  5807  1stvalg  6197  2ndvalg  6198  fo1st  6212  fo2nd  6213  f1stres  6214  f2ndres  6215  2nd1st  6235  cnvf1olem  6279  brtpos2  6306  dftpos4  6318  tpostpos  6319  recseq  6361  tfrexlem  6389  ixpsnf1o  6792  xpcomco  6882  xpassen  6886  xpdom2  6887  supeq1  7047  supeq2  7050  supeq3  7051  supeq123d  7052  en2other2  7258  dfinfre  8977  hashinfom  10852  hashennn  10854  fsumcnv  11583  fprodcnv  11771  tgval  12876  ptex  12878  lssuni  13862  lspuni0  13923  lss0v  13929  zrhval  14116  zrhvalg  14117  zrhval2  14118  zrhpropd  14125  isbasisg  14223  basis1  14226  baspartn  14229  eltg  14231  ntrfval  14279  ntrval  14289  tgrest  14348  restuni2  14356  lmfval  14371  cnfval  14373  cnpfval  14374  txtopon  14441  txswaphmeolem  14499  peano4nninf  15566