Theorem uneq1d 4166

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151

This theorem is used by:  ifeq1  4485  preq1  4690  tpeq1  4699  tpeq2  4700  tpprceq3  4763  iunxdif3  5054  iununi  5058  resasplit  6753  fresaunres2  6755  fmptpr  7178  funresdfunsn  7195  ressuppssdif  8206  on2recsov  8681  sbthlem5  9114  fodomr  9151  domunfican  9317  fodomfir  9323  brwdom2  9571  rankung  9877  ackbij1lem2  10302  ttukeylem3  10593  snunioo  13613  snunioc  13615  prunioo  13616  fzpred  13710  fseq1p1m1  13736  nn0split  13781  fz0sn0fz1  13783  fzo0sn0fzo1  13894  fzosplitpr  13916  s2prop  15064  s4prop  15067  fsum1p  15925  fprod1p  16141  setsval  17351  setsabs  17363  setscom  17364  prdsval  17632  prdsdsval  17655  prdsdsval2  17661  prdsdsval3  17662  mreexexlem3d  17826  mreexexlem4d  17827  estrres  18319  symg2bas  19613  symgvalstruct  19617  evlseu  22398  ordtuni  23514  lfinun  23850  alexsubALTlem3  24374  ustssco  24540  trust  24554  ressprdsds  24696  xpsdsval  24706  nulmbl2  25863  uniioombllem3  25912  uniioombllem4  25913  plyeq0  26536  plyaddlem1  26538  plymullem1  26539  fta1lem  26634  vieta1lem2  26640  birthdaylem2  27286  noetasuplem2  28097  noxpordpred  28345  addsproplem1  28361  addsprop  28368  negsproplem1  28420  negsprop  28427  mulsproplemcbv  28507  mulsproplem1  28508  mulsprop  28522  precsexlemcbv  28598  precsexlem3  28601  edglnl  29727  iuninc  33203  nn0diffz0  33433  pmtrcnel2  33698  tocycval  33716  cycpmco2rn  33733  dflringlem3  34075  dflring4  34077  evlextv  34221  difelcarsg  34989  actfunsnf1o  35280  reprsuc  35291  breprexplema  35306  bnj1416  35716  mclsval  36415  mclsax  36421  topjoin  37246  ttcsng  37400  ttcsntrsucg  37403  bj-tageq  37982  finixpnum  38622  poimirlem3  38635  poimirlem4  38636  poimirlem6  38638  poimirlem7  38639  poimirlem9  38641  poimirlem16  38648  poimirlem17  38649  poimirlem28  38660  mblfinlem2  38670  islshpsm  40131  lshpnel2N  40136  lkrlsp3  40255  pclfinclN  41101  dochsatshp  42602  mapfzcons1  43822  iunrelexp0  44796  isotone1  45142  fiiuncl  46176  nnsplit  46464  fourierdlem32  47243  fzopred  48487  fzopredsuc  48488  dfsclnbgr6  49050  aacllem  51108