Theorem uneq1d 4121

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

Syntax hints:   → wi 4   = wceq 1570   ∪ cun 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910

This theorem is referenced by:  ifeq1  4491  preq1  4699  tpeq1  4708  tpeq2  4709  tpprceq3  4772  iunxdif3  5061  iununi  5065  resasplit  6748  fresaunres2  6750  fmptpr  7170  funresdfunsn  7187  ressuppssdif  8177  on2recsov  8650  sbthlem5  9075  fodomr  9112  domunfican  9277  fodomfir  9283  brwdom2  9531  ackbij1lem2  10199  ttukeylem3  10490  snunioo  13500  snunioc  13502  prunioo  13503  fzpred  13596  fseq1p1m1  13622  nn0split  13667  fz0sn0fz1  13669  fzo0sn0fzo1  13780  fzosplitpr  13802  s2prop  14940  s4prop  14943  fsum1p  15800  fprod1p  16018  setsval  17222  setsabs  17234  setscom  17235  prdsval  17503  prdsdsval  17526  prdsdsval2  17532  prdsdsval3  17533  mreexexlem3d  17697  mreexexlem4d  17698  estrres  18190  symg2bas  19458  symgvalstruct  19462  evlseu  22234  ordtuni  23347  lfinun  23682  alexsubALTlem3  24206  ustssco  24372  trust  24386  ressprdsds  24528  xpsdsval  24538  nulmbl2  25695  uniioombllem3  25744  uniioombllem4  25745  plyeq0  26368  plyaddlem1  26370  plymullem1  26371  fta1lem  26468  vieta1lem2  26472  birthdaylem2  27117  noetasuplem2  27898  noxpordpred  28146  addsproplem1  28162  addsprop  28169  negsproplem1  28221  negsprop  28228  mulsproplemcbv  28308  mulsproplem1  28309  mulsprop  28323  precsexlemcbv  28399  precsexlem3  28402  edglnl  29493  iuninc  32905  nn0diffz0  33139  pmtrcnel2  33410  tocycval  33428  cycpmco2rn  33445  dflringlem3  33786  dflring4  33788  evlextv  33932  difelcarsg  34700  actfunsnf1o  34991  reprsuc  35002  breprexplema  35017  bnj1416  35427  mclsval  36055  mclsax  36061  rankung  36658  topjoin  36876  ttcsng  37030  ttcsntrsucg  37033  bj-tageq  37612  finixpnum  38256  poimirlem3  38274  poimirlem4  38275  poimirlem6  38277  poimirlem7  38278  poimirlem9  38280  poimirlem16  38287  poimirlem17  38288  poimirlem28  38299  mblfinlem2  38309  islshpsm  39754  lshpnel2N  39759  lkrlsp3  39878  pclfinclN  40724  dochsatshp  42225  mapfzcons1  43448  iunrelexp0  44428  isotone1  44774  fiiuncl  45785  nnsplit  46074  fourierdlem32  46853  fzopred  48060  fzopredsuc  48061  dfsclnbgr6  48623  aacllem  50621