Theorem uneq1d 4190

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

Syntax hints:   → wi 4   = wceq 1537   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981

This theorem is referenced by:  ifeq1  4552  preq1  4758  tpeq1  4767  tpeq2  4768  tpprceq3  4829  iunxdif3  5118  iununi  5122  resasplit  6791  fresaunres2  6793  fmptpr  7206  funresdfunsn  7223  ressuppssdif  8226  on2recsov  8724  sbthlem5  9153  fodomr  9194  domunfican  9389  fodomfir  9396  brwdom2  9642  ackbij1lem2  10289  ttukeylem3  10580  snunioo  13538  snunioc  13540  prunioo  13541  fzpred  13632  fseq1p1m1  13658  nn0split  13700  fz0sn0fz1  13702  fzo0sn0fzo1  13805  fzosplitpr  13826  s2prop  14956  s4prop  14959  fsum1p  15801  fprod1p  16016  setsval  17214  setsabs  17226  setscom  17227  prdsval  17515  prdsdsval  17538  prdsdsval2  17544  prdsdsval3  17545  mreexexlem3d  17704  mreexexlem4d  17705  estrres  18208  symg2bas  19434  symgvalstruct  19438  symgvalstructOLD  19439  evlseu  22130  ordtuni  23219  lfinun  23554  alexsubALTlem3  24078  ustssco  24244  trust  24259  ressprdsds  24402  xpsdsval  24412  nulmbl2  25590  uniioombllem3  25639  uniioombllem4  25640  plyeq0  26270  plyaddlem1  26272  plymullem1  26273  fta1lem  26367  vieta1lem2  26371  birthdaylem2  27013  noetasuplem2  27797  noxpordpred  28004  addsproplem1  28020  addsprop  28027  negsproplem1  28078  negsprop  28085  mulsproplemcbv  28159  mulsproplem1  28160  mulsprop  28174  precsexlemcbv  28248  precsexlem3  28251  edglnl  29178  iuninc  32583  pmtrcnel2  33083  tocycval  33101  cycpmco2rn  33118  difelcarsg  34275  actfunsnf1o  34581  reprsuc  34592  breprexplema  34607  bnj1416  35015  mclsval  35531  mclsax  35537  rankung  36130  topjoin  36331  bj-tageq  36942  finixpnum  37565  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem9  37589  poimirlem16  37596  poimirlem17  37597  poimirlem28  37608  mblfinlem2  37618  islshpsm  38936  lshpnel2N  38941  lkrlsp3  39060  pclfinclN  39907  dochsatshp  41408  metakunt24  42185  mapfzcons1  42673  iunrelexp0  43664  isotone1  44010  fiiuncl  44967  nnsplit  45273  fourierdlem32  46060  fzopred  47237  fzopredsuc  47238  dfsclnbgr6  47730  aacllem  48895