Theorem unieqd 3846

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

Syntax hints:   -> wi 4   = wceq 1364   U.cuni 3835

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-uni 3836

This theorem is referenced by:  uniprg  3850  unisng  3852  unisn3  4476  onsucuni2  4596  opswapg  5152  elxp4  5153  elxp5  5154  iotaeq  5223  iotabi  5224  uniabio  5225  funfvdm  5620  funfvdm2  5621  fvun1  5623  fniunfv  5805  funiunfvdm  5806  1stvalg  6195  2ndvalg  6196  fo1st  6210  fo2nd  6211  f1stres  6212  f2ndres  6213  2nd1st  6233  cnvf1olem  6277  brtpos2  6304  dftpos4  6316  tpostpos  6317  recseq  6359  tfrexlem  6387  ixpsnf1o  6790  xpcomco  6880  xpassen  6884  xpdom2  6885  supeq1  7045  supeq2  7048  supeq3  7049  supeq123d  7050  en2other2  7256  dfinfre  8975  hashinfom  10849  hashennn  10851  fsumcnv  11580  fprodcnv  11768  tgval  12873  ptex  12875  lssuni  13859  lspuni0  13920  lss0v  13926  zrhval  14105  zrhvalg  14106  zrhval2  14107  zrhpropd  14114  isbasisg  14212  basis1  14215  baspartn  14218  eltg  14220  ntrfval  14268  ntrval  14278  tgrest  14337  restuni2  14345  lmfval  14360  cnfval  14362  cnpfval  14363  txtopon  14430  txswaphmeolem  14488  peano4nninf  15496