Theorem uneq1d 4108

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-un 3902

This theorem is referenced by:  ifeq1  4476  preq1  4680  tpeq1  4689  tpeq2  4690  tpprceq3  4750  iunxdif3  5039  iununi  5043  resasplit  6689  fresaunres2  6691  fmptpr  7094  funresdfunsn  7111  ressuppssdif  8063  sbthlem5  8944  fodomr  8985  domunfican  9177  brwdom2  9422  ackbij1lem2  10070  ttukeylem3  10360  snunioo  13303  snunioc  13305  prunioo  13306  fzpred  13397  fseq1p1m1  13423  nn0split  13464  fz0sn0fz1  13466  fzo0sn0fzo1  13569  fzosplitpr  13589  s2prop  14711  s4prop  14714  fsum1p  15556  fprod1p  15769  setsval  16957  setsabs  16969  setscom  16970  prdsval  17255  prdsdsval  17278  prdsdsval2  17284  prdsdsval3  17285  mreexexlem3d  17444  mreexexlem4d  17445  estrres  17945  symg2bas  19088  symgvalstruct  19092  symgvalstructOLD  19093  evlseu  21391  ordtuni  22439  lfinun  22774  alexsubALTlem3  23298  ustssco  23464  trust  23479  ressprdsds  23622  xpsdsval  23632  nulmbl2  24798  uniioombllem3  24847  uniioombllem4  24848  plyeq0  25470  plyaddlem1  25472  plymullem1  25473  fta1lem  25565  vieta1lem2  25569  birthdaylem2  26200  noetasuplem2  26980  edglnl  27743  iuninc  31128  pmtrcnel2  31587  tocycval  31603  cycpmco2rn  31620  difelcarsg  32518  actfunsnf1o  32825  reprsuc  32836  breprexplema  32851  bnj1416  33259  mclsval  33765  mclsax  33771  on2recsov  34050  noxpordpred  34201  rankung  34559  topjoin  34645  bj-tageq  35255  finixpnum  35860  poimirlem3  35878  poimirlem4  35879  poimirlem6  35881  poimirlem7  35882  poimirlem9  35884  poimirlem16  35891  poimirlem17  35892  poimirlem28  35903  mblfinlem2  35913  islshpsm  37240  lshpnel2N  37245  lkrlsp3  37364  pclfinclN  38211  dochsatshp  39712  metakunt24  40398  mapfzcons1  40789  iunrelexp0  41620  isotone1  41968  fiiuncl  42922  nnsplit  43221  fourierdlem32  44005  fzopred  45154  fzopredsuc  45155  aacllem  46845