Theorem uneq1d 4092

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888

This theorem is referenced by:  ifeq1  4460  preq1  4666  tpeq1  4675  tpeq2  4676  tpprceq3  4734  iunxdif3  5020  iununi  5024  resasplit  6628  fresaunres2  6630  fmptpr  7026  funresdfunsn  7043  ressuppssdif  7972  sbthlem5  8827  fodomr  8864  domunfican  9017  brwdom2  9262  ackbij1lem2  9908  ttukeylem3  10198  snunioo  13139  snunioc  13141  prunioo  13142  fzpred  13233  fseq1p1m1  13259  nn0split  13300  fz0sn0fz1  13302  fzo0sn0fzo1  13404  fzosplitpr  13424  s2prop  14548  s4prop  14551  fsum1p  15393  fprod1p  15606  setsval  16796  setsabs  16808  setscom  16809  prdsval  17083  prdsdsval  17106  prdsdsval2  17112  prdsdsval3  17113  mreexexlem3d  17272  mreexexlem4d  17273  estrres  17772  symg2bas  18915  symgvalstruct  18919  symgvalstructOLD  18920  evlseu  21203  ordtuni  22249  lfinun  22584  alexsubALTlem3  23108  ustssco  23274  trust  23289  ressprdsds  23432  xpsdsval  23442  nulmbl2  24605  uniioombllem3  24654  uniioombllem4  24655  plyeq0  25277  plyaddlem1  25279  plymullem1  25280  fta1lem  25372  vieta1lem2  25376  birthdaylem2  26007  edglnl  27416  iuninc  30801  pmtrcnel2  31261  tocycval  31277  cycpmco2rn  31294  difelcarsg  32177  actfunsnf1o  32484  reprsuc  32495  breprexplema  32510  bnj1416  32919  mclsval  33425  mclsax  33431  on2recsov  33754  noetasuplem2  33864  noxpordpred  34037  rankung  34395  topjoin  34481  bj-tageq  35093  finixpnum  35689  poimirlem3  35707  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem9  35713  poimirlem16  35720  poimirlem17  35721  poimirlem28  35732  mblfinlem2  35742  islshpsm  36921  lshpnel2N  36926  lkrlsp3  37045  pclfinclN  37891  dochsatshp  39392  metakunt24  40076  mapfzcons1  40455  iunrelexp0  41199  isotone1  41547  fiiuncl  42502  nnsplit  42787  fourierdlem32  43570  fzopred  44702  fzopredsuc  44703  aacllem  46391