Theorem unieqd 3899

Description: Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)

Hypothesis

Ref	Expression
unieqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
unieqd	⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)

Proof of Theorem unieqd

Step	Hyp	Ref	Expression
1		unieqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		unieq 3897	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1395  ∪ cuni 3888

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-uni 3889

This theorem is referenced by:  uniprg  3903  unisng  3905  unisn3  4536  onsucuni2  4656  opswapg  5215  elxp4  5216  elxp5  5217  iotaeq  5287  iotabi  5288  uniabio  5289  funfvdm  5699  funfvdm2  5700  fvun1  5702  fniunfv  5892  funiunfvdm  5893  1stvalg  6294  2ndvalg  6295  fo1st  6309  fo2nd  6310  f1stres  6311  f2ndres  6312  2nd1st  6332  cnvf1olem  6376  brtpos2  6403  dftpos4  6415  tpostpos  6416  recseq  6458  tfrexlem  6486  ixpsnf1o  6891  xpcomco  6993  xpassen  6997  xpdom2  6998  supeq1  7164  supeq2  7167  supeq3  7168  supeq123d  7169  en2other2  7385  dfinfre  9114  hashinfom  11012  hashennn  11014  fsumcnv  11964  fprodcnv  12152  tgval  13311  ptex  13313  lssuni  14343  lspuni0  14404  lss0v  14410  zrhval  14597  zrhvalg  14598  zrhval2  14599  zrhpropd  14606  isbasisg  14734  basis1  14737  baspartn  14740  eltg  14742  ntrfval  14790  ntrval  14800  tgrest  14859  restuni2  14867  lmfval  14883  cnfval  14884  cnpfval  14885  txtopon  14952  txswaphmeolem  15010  peano4nninf  16460