Theorem unieqd 3861

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 3859	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1373  ∪ cuni 3850

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-uni 3851

This theorem is referenced by:  uniprg  3865  unisng  3867  unisn3  4492  onsucuni2  4612  opswapg  5169  elxp4  5170  elxp5  5171  iotaeq  5240  iotabi  5241  uniabio  5242  funfvdm  5642  funfvdm2  5643  fvun1  5645  fniunfv  5831  funiunfvdm  5832  1stvalg  6228  2ndvalg  6229  fo1st  6243  fo2nd  6244  f1stres  6245  f2ndres  6246  2nd1st  6266  cnvf1olem  6310  brtpos2  6337  dftpos4  6349  tpostpos  6350  recseq  6392  tfrexlem  6420  ixpsnf1o  6823  xpcomco  6921  xpassen  6925  xpdom2  6926  supeq1  7088  supeq2  7091  supeq3  7092  supeq123d  7093  en2other2  7304  dfinfre  9029  hashinfom  10923  hashennn  10925  fsumcnv  11748  fprodcnv  11936  tgval  13094  ptex  13096  lssuni  14125  lspuni0  14186  lss0v  14192  zrhval  14379  zrhvalg  14380  zrhval2  14381  zrhpropd  14388  isbasisg  14516  basis1  14519  baspartn  14522  eltg  14524  ntrfval  14572  ntrval  14582  tgrest  14641  restuni2  14649  lmfval  14664  cnfval  14666  cnpfval  14667  txtopon  14734  txswaphmeolem  14792  peano4nninf  15943