Theorem uneq1d 4147

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

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936

This theorem is referenced by:  ifeq1  4509  preq1  4714  tpeq1  4723  tpeq2  4724  tpprceq3  4785  iunxdif3  5076  iununi  5080  resasplit  6753  fresaunres2  6755  fmptpr  7169  funresdfunsn  7186  ressuppssdif  8189  on2recsov  8685  sbthlem5  9106  fodomr  9147  domunfican  9338  fodomfir  9345  brwdom2  9592  ackbij1lem2  10239  ttukeylem3  10530  snunioo  13500  snunioc  13502  prunioo  13503  fzpred  13594  fseq1p1m1  13620  nn0split  13665  fz0sn0fz1  13667  fzo0sn0fzo1  13776  fzosplitpr  13797  s2prop  14931  s4prop  14934  fsum1p  15774  fprod1p  15989  setsval  17191  setsabs  17203  setscom  17204  prdsval  17474  prdsdsval  17497  prdsdsval2  17503  prdsdsval3  17504  mreexexlem3d  17663  mreexexlem4d  17664  estrres  18156  symg2bas  19379  symgvalstruct  19383  evlseu  22046  ordtuni  23133  lfinun  23468  alexsubALTlem3  23992  ustssco  24158  trust  24173  ressprdsds  24315  xpsdsval  24325  nulmbl2  25494  uniioombllem3  25543  uniioombllem4  25544  plyeq0  26173  plyaddlem1  26175  plymullem1  26176  fta1lem  26272  vieta1lem2  26276  birthdaylem2  26919  noetasuplem2  27703  noxpordpred  27917  addsproplem1  27933  addsprop  27940  negsproplem1  27991  negsprop  27998  mulsproplemcbv  28075  mulsproplem1  28076  mulsprop  28090  precsexlemcbv  28165  precsexlem3  28168  edglnl  29127  iuninc  32546  pmtrcnel2  33106  tocycval  33124  cycpmco2rn  33141  difelcarsg  34347  actfunsnf1o  34641  reprsuc  34652  breprexplema  34667  bnj1416  35075  mclsval  35590  mclsax  35596  rankung  36189  topjoin  36388  bj-tageq  36999  finixpnum  37634  poimirlem3  37652  poimirlem4  37653  poimirlem6  37655  poimirlem7  37656  poimirlem9  37658  poimirlem16  37665  poimirlem17  37666  poimirlem28  37677  mblfinlem2  37687  islshpsm  39003  lshpnel2N  39008  lkrlsp3  39127  pclfinclN  39974  dochsatshp  41475  mapfzcons1  42707  iunrelexp0  43693  isotone1  44039  fiiuncl  45056  nnsplit  45352  fourierdlem32  46135  fzopred  47318  fzopredsuc  47319  dfsclnbgr6  47838  aacllem  49632