Theorem unieqd 3904

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

Syntax hints:   -> wi 4   = wceq 1397   U.cuni 3893

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-uni 3894

This theorem is referenced by:  uniprg  3908  unisng  3910  unisn3  4542  onsucuni2  4662  opswapg  5223  elxp4  5224  elxp5  5225  iotaeq  5295  iotabi  5296  uniabio  5297  funfvdm  5709  funfvdm2  5710  fvun1  5712  fniunfv  5903  funiunfvdm  5904  1stvalg  6305  2ndvalg  6306  fo1st  6320  fo2nd  6321  f1stres  6322  f2ndres  6323  2nd1st  6343  cnvf1olem  6389  brtpos2  6417  dftpos4  6429  tpostpos  6430  recseq  6472  tfrexlem  6500  ixpsnf1o  6905  xpcomco  7010  xpassen  7014  xpdom2  7015  supeq1  7185  supeq2  7188  supeq3  7189  supeq123d  7190  en2other2  7407  dfinfre  9136  hashinfom  11041  hashennn  11043  fsumcnv  12016  fprodcnv  12204  tgval  13363  ptex  13365  lssuni  14396  lspuni0  14457  lss0v  14463  zrhval  14650  zrhvalg  14651  zrhval2  14652  zrhpropd  14659  isbasisg  14787  basis1  14790  baspartn  14793  eltg  14795  ntrfval  14843  ntrval  14853  tgrest  14912  restuni2  14920  lmfval  14936  cnfval  14937  cnpfval  14938  txtopon  15005  txswaphmeolem  15063  peano4nninf  16659