Theorem uneq1d 4129

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

Syntax hints:   → wi 4   = wceq 1567   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918

This theorem is referenced by:  ifeq1  4493  preq1  4701  tpeq1  4710  tpeq2  4711  tpprceq3  4773  iunxdif3  5062  iununi  5066  resasplit  6746  fresaunres2  6748  fmptpr  7168  funresdfunsn  7185  ressuppssdif  8177  on2recsov  8650  sbthlem5  9075  fodomr  9112  domunfican  9277  fodomfir  9283  brwdom2  9531  ackbij1lem2  10199  ttukeylem3  10491  snunioo  13501  snunioc  13503  prunioo  13504  fzpred  13596  fseq1p1m1  13622  nn0split  13667  fz0sn0fz1  13669  fzo0sn0fzo1  13780  fzosplitpr  13802  s2prop  14940  s4prop  14943  fsum1p  15800  fprod1p  16018  setsval  17223  setsabs  17235  setscom  17236  prdsval  17504  prdsdsval  17527  prdsdsval2  17533  prdsdsval3  17534  mreexexlem3d  17698  mreexexlem4d  17699  estrres  18191  symg2bas  19459  symgvalstruct  19463  evlseu  22199  ordtuni  23312  lfinun  23647  alexsubALTlem3  24171  ustssco  24337  trust  24351  ressprdsds  24493  xpsdsval  24503  nulmbl2  25660  uniioombllem3  25709  uniioombllem4  25710  plyeq0  26333  plyaddlem1  26335  plymullem1  26336  fta1lem  26433  vieta1lem2  26437  birthdaylem2  27079  noetasuplem2  27860  noxpordpred  28108  addsproplem1  28124  addsprop  28131  negsproplem1  28183  negsprop  28190  mulsproplemcbv  28270  mulsproplem1  28271  mulsprop  28285  precsexlemcbv  28361  precsexlem3  28364  edglnl  29430  iuninc  32842  nn0diffz0  33076  pmtrcnel2  33347  tocycval  33365  cycpmco2rn  33382  dflringlem3  33727  dflring4  33729  evlextv  33873  difelcarsg  34641  actfunsnf1o  34932  reprsuc  34943  breprexplema  34958  bnj1416  35368  mclsval  35950  mclsax  35956  rankung  36553  topjoin  36761  ttcsng  36915  ttcsntrsucg  36918  bj-tageq  37496  finixpnum  38139  poimirlem3  38157  poimirlem4  38158  poimirlem6  38160  poimirlem7  38161  poimirlem9  38163  poimirlem16  38170  poimirlem17  38171  poimirlem28  38182  mblfinlem2  38192  islshpsm  39639  lshpnel2N  39644  lkrlsp3  39763  pclfinclN  40609  dochsatshp  42110  mapfzcons1  43333  iunrelexp0  44313  isotone1  44659  fiiuncl  45670  nnsplit  45959  fourierdlem32  46738  fzopred  47942  fzopredsuc  47943  dfsclnbgr6  48505  aacllem  50457