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  4591  onsucuni2  4711  opswapg  5274  elxp4  5275  elxp5  5276  iotaeq  5346  iotabi  5347  uniabio  5348  funfvdm  5766  funfvdm2  5767  fvun1  5769  fniunfv  5968  funiunfvdm  5969  1stvalg  6376  2ndvalg  6377  fo1st  6391  fo2nd  6392  f1stres  6393  f2ndres  6394  2nd1st  6414  cnvf1olem  6460  brtpos2  6522  dftpos4  6534  tpostpos  6535  recseq  6577  tfrexlem  6605  ixpsnf1o  7018  xpcomco  7124  xpassen  7128  xpdom2  7129  supeq1  7327  supeq2  7330  supeq3  7331  supeq123d  7332  en2other2  7549  dfinfre  9289  hashinfom  11232  hashennn  11234  fsumcnv  12222  fprodcnv  12410  tgval  13667  ptex  13669  lssuni  14751  lspuni0  14812  lss0v  14818  zrhval  15003  zrhvalg  15004  zrhval2  15005  zrhpropd  15012  isbasisg  15197  basis1  15200  baspartn  15203  eltg  15205  ntrfval  15253  ntrval  15263  tgrest  15322  restuni2  15330  lmfval  15346  cnfval  15347  cnpfval  15348  txtopon  15415  txswaphmeolem  15473  peano4nninf  17171