Theorem uneq1d 4162

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

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

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 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3953

This theorem is referenced by:  ifeq1  4532  preq1  4737  tpeq1  4746  tpeq2  4747  tpprceq3  4807  iunxdif3  5098  iununi  5102  resasplit  6761  fresaunres2  6763  fmptpr  7172  funresdfunsn  7189  ressuppssdif  8175  on2recsov  8673  sbthlem5  9093  fodomr  9134  domunfican  9326  brwdom2  9574  ackbij1lem2  10222  ttukeylem3  10512  snunioo  13462  snunioc  13464  prunioo  13465  fzpred  13556  fseq1p1m1  13582  nn0split  13623  fz0sn0fz1  13625  fzo0sn0fzo1  13728  fzosplitpr  13748  s2prop  14865  s4prop  14868  fsum1p  15706  fprod1p  15919  setsval  17107  setsabs  17119  setscom  17120  prdsval  17408  prdsdsval  17431  prdsdsval2  17437  prdsdsval3  17438  mreexexlem3d  17597  mreexexlem4d  17598  estrres  18101  symg2bas  19308  symgvalstruct  19312  symgvalstructOLD  19313  evlseu  21957  ordtuni  23014  lfinun  23349  alexsubALTlem3  23873  ustssco  24039  trust  24054  ressprdsds  24197  xpsdsval  24207  nulmbl2  25385  uniioombllem3  25434  uniioombllem4  25435  plyeq0  26063  plyaddlem1  26065  plymullem1  26066  fta1lem  26159  vieta1lem2  26163  birthdaylem2  26798  noetasuplem2  27580  noxpordpred  27783  addsproplem1  27799  addsprop  27806  negsproplem1  27853  negsprop  27860  mulsproplemcbv  27928  mulsproplem1  27929  mulsprop  27943  precsexlemcbv  28017  precsexlem3  28020  edglnl  28836  iuninc  32225  pmtrcnel2  32687  tocycval  32703  cycpmco2rn  32720  difelcarsg  33773  actfunsnf1o  34080  reprsuc  34091  breprexplema  34106  bnj1416  34514  mclsval  35018  mclsax  35024  rankung  35608  topjoin  35714  bj-tageq  36321  finixpnum  36937  poimirlem3  36955  poimirlem4  36956  poimirlem6  36958  poimirlem7  36959  poimirlem9  36961  poimirlem16  36968  poimirlem17  36969  poimirlem28  36980  mblfinlem2  36990  islshpsm  38314  lshpnel2N  38319  lkrlsp3  38438  pclfinclN  39285  dochsatshp  40786  metakunt24  41475  mapfzcons1  41918  iunrelexp0  42916  isotone1  43262  fiiuncl  44214  nnsplit  44527  fourierdlem32  45314  fzopred  46489  fzopredsuc  46490  aacllem  48010