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  7326  supeq2  7329  supeq3  7330  supeq123d  7331  en2other2  7548  dfinfre  9286  hashinfom  11217  hashennn  11219  fsumcnv  12204  fprodcnv  12392  tgval  13616  ptex  13618  lssuni  14700  lspuni0  14761  lss0v  14767  zrhval  14952  zrhvalg  14953  zrhval2  14954  zrhpropd  14961  isbasisg  15145  basis1  15148  baspartn  15151  eltg  15153  ntrfval  15201  ntrval  15211  tgrest  15270  restuni2  15278  lmfval  15294  cnfval  15295  cnpfval  15296  txtopon  15363  txswaphmeolem  15421  peano4nninf  17049