Theorem uneq1d 3728

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

Syntax hints:   → wi 4   = wceq 1475   ∪ cun 3538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545

This theorem is referenced by:  ifeq1  4040  preq1  4212  tpeq1  4221  tpeq2  4222  tpprceq3  4276  iunxdif3  4542  iununi  4546  resasplit  5987  fresaunres2  5989  fmptpr  6343  funresdfunsn  6360  ressuppssdif  7203  sbthlem5  7959  fodomr  7996  domunfican  8118  brwdom2  8361  cdaval  8875  ackbij1lem2  8926  ttukeylem3  9216  snunioo  12169  snunioc  12171  prunioo  12172  fzpred  12259  fseq1p1m1  12283  nn0split  12323  fz0sn0fz1  12325  fzo0sn0fzo1  12424  fzosplitprm1  12443  s2prop  13502  s4prop  13505  fsum1p  14326  fprod1p  14537  setsval  15720  setsabs  15730  setscom  15731  prdsval  15938  prdsdsval  15961  prdsdsval2  15967  prdsdsval3  15968  mreexexlem3d  16129  mreexexlem4d  16130  estrres  16602  symg2bas  17641  evlseu  19337  ordtuni  20804  lfinun  21138  alexsubALTlem3  21663  ustssco  21828  trust  21843  ressprdsds  21986  xpsdsval  21996  nulmbl2  23111  uniioombllem3  23159  uniioombllem4  23160  plyeq0  23771  plyaddlem1  23773  plymullem1  23774  fta1lem  23866  vieta1lem2  23870  birthdaylem2  24479  nbgraopALT  25953  iuninc  28761  difelcarsg  29699  bnj1416  30361  mclsval  30714  mclsax  30720  rankung  31443  topjoin  31530  bj-tageq  32157  finixpnum  32564  poimirlem3  32582  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem9  32588  poimirlem16  32595  poimirlem17  32596  poimirlem28  32607  mblfinlem2  32617  islshpsm  33285  lshpnel2N  33290  lkrlsp3  33409  pclfinclN  34254  dochsatshp  35758  mapfzcons1  36298  iunrelexp0  37013  isotone1  37366  fiiuncl  38259  nnsplit  38515  fourierdlem32  39032  fzopred  39945  fzopredsuc  39946  fzosplitpr  40362  aacllem  42356