Theorem uneq1d 4166

Description: Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.)

Hypothesis

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

Assertion

Ref	Expression
uneq1d	⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Proof of Theorem uneq1d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		uneq1 4160	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   = wceq 1539   ∪ cun 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955

This theorem is referenced by:  ifeq1  4528  preq1  4732  tpeq1  4741  tpeq2  4742  tpprceq3  4803  iunxdif3  5094  iununi  5098  resasplit  6777  fresaunres2  6779  fmptpr  7193  funresdfunsn  7210  ressuppssdif  8211  on2recsov  8707  sbthlem5  9128  fodomr  9169  domunfican  9362  fodomfir  9369  brwdom2  9614  ackbij1lem2  10261  ttukeylem3  10552  snunioo  13519  snunioc  13521  prunioo  13522  fzpred  13613  fseq1p1m1  13639  nn0split  13684  fz0sn0fz1  13686  fzo0sn0fzo1  13795  fzosplitpr  13816  s2prop  14947  s4prop  14950  fsum1p  15790  fprod1p  16005  setsval  17205  setsabs  17217  setscom  17218  prdsval  17501  prdsdsval  17524  prdsdsval2  17530  prdsdsval3  17531  mreexexlem3d  17690  mreexexlem4d  17691  estrres  18185  symg2bas  19411  symgvalstruct  19415  symgvalstructOLD  19416  evlseu  22108  ordtuni  23199  lfinun  23534  alexsubALTlem3  24058  ustssco  24224  trust  24239  ressprdsds  24382  xpsdsval  24392  nulmbl2  25572  uniioombllem3  25621  uniioombllem4  25622  plyeq0  26251  plyaddlem1  26253  plymullem1  26254  fta1lem  26350  vieta1lem2  26354  birthdaylem2  26996  noetasuplem2  27780  noxpordpred  27987  addsproplem1  28003  addsprop  28010  negsproplem1  28061  negsprop  28068  mulsproplemcbv  28142  mulsproplem1  28143  mulsprop  28157  precsexlemcbv  28231  precsexlem3  28234  edglnl  29161  iuninc  32574  pmtrcnel2  33111  tocycval  33129  cycpmco2rn  33146  difelcarsg  34313  actfunsnf1o  34620  reprsuc  34631  breprexplema  34646  bnj1416  35054  mclsval  35569  mclsax  35575  rankung  36168  topjoin  36367  bj-tageq  36978  finixpnum  37613  poimirlem3  37631  poimirlem4  37632  poimirlem6  37634  poimirlem7  37635  poimirlem9  37637  poimirlem16  37644  poimirlem17  37645  poimirlem28  37656  mblfinlem2  37666  islshpsm  38982  lshpnel2N  38987  lkrlsp3  39106  pclfinclN  39953  dochsatshp  41454  metakunt24  42230  mapfzcons1  42733  iunrelexp0  43720  isotone1  44066  fiiuncl  45075  nnsplit  45374  fourierdlem32  46159  fzopred  47339  fzopredsuc  47340  dfsclnbgr6  47849  aacllem  49375