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  4593  onsucuni2  4713  opswapg  5277  elxp4  5278  elxp5  5279  iotaeq  5349  iotabi  5350  uniabio  5351  funfvdm  5769  funfvdm2  5770  fvun1  5772  fniunfv  5971  funiunfvdm  5972  1stvalg  6380  2ndvalg  6381  fo1st  6395  fo2nd  6396  f1stres  6397  f2ndres  6398  2nd1st  6418  cnvf1olem  6464  brtpos2  6526  dftpos4  6538  tpostpos  6539  recseq  6581  tfrexlem  6609  ixpsnf1o  7022  xpcomco  7128  xpassen  7132  xpdom2  7133  supeq1  7332  supeq2  7335  supeq3  7336  supeq123d  7337  en2other2  7554  dfinfre  9294  hashinfom  11239  hashennn  11241  fsumcnv  12229  fprodcnv  12417  tgval  13675  ptex  13677  gsumcom2fi  14275  lssuni  14809  lspuni0  14870  lss0v  14876  zrhval  15061  zrhvalg  15062  zrhval2  15063  zrhpropd  15070  isbasisg  15270  basis1  15273  baspartn  15276  eltg  15278  ntrfval  15326  ntrval  15336  tgrest  15395  restuni2  15403  lmfval  15419  cnfval  15420  cnpfval  15421  txtopon  15488  txswaphmeolem  15546  peano4nninf  17255