Theorem unieqd 3821

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

Syntax hints:   -> wi 4   = wceq 1353   U.cuni 3810

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3811

This theorem is referenced by:  uniprg  3825  unisng  3827  unisn3  4446  onsucuni2  4564  opswapg  5116  elxp4  5117  elxp5  5118  iotaeq  5187  iotabi  5188  uniabio  5189  funfvdm  5580  funfvdm2  5581  fvun1  5583  fniunfv  5763  funiunfvdm  5764  1stvalg  6143  2ndvalg  6144  fo1st  6158  fo2nd  6159  f1stres  6160  f2ndres  6161  2nd1st  6181  cnvf1olem  6225  brtpos2  6252  dftpos4  6264  tpostpos  6265  recseq  6307  tfrexlem  6335  ixpsnf1o  6736  xpcomco  6826  xpassen  6830  xpdom2  6831  supeq1  6985  supeq2  6988  supeq3  6989  supeq123d  6990  en2other2  7195  dfinfre  8913  hashinfom  10758  hashennn  10760  fsumcnv  11445  fprodcnv  11633  tgval  12711  ptex  12713  isbasisg  13547  basis1  13550  baspartn  13553  eltg  13555  ntrfval  13603  ntrval  13613  tgrest  13672  restuni2  13680  lmfval  13695  cnfval  13697  cnpfval  13698  txtopon  13765  txswaphmeolem  13823  peano4nninf  14758