Theorem uneq1d 4114

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∪ cun 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904

This theorem is used by:  ifeq1  4486  preq1  4694  tpeq1  4703  tpeq2  4704  tpprceq3  4767  iunxdif3  5055  iununi  5059  resasplit  6745  fresaunres2  6747  fmptpr  7170  funresdfunsn  7187  ressuppssdif  8183  on2recsov  8656  sbthlem5  9089  fodomr  9126  domunfican  9291  fodomfir  9297  brwdom2  9545  ackbij1lem2  10222  ttukeylem3  10513  snunioo  13531  snunioc  13533  prunioo  13534  fzpred  13627  fseq1p1m1  13653  nn0split  13698  fz0sn0fz1  13700  fzo0sn0fzo1  13811  fzosplitpr  13833  s2prop  14978  s4prop  14981  fsum1p  15839  fprod1p  16055  setsval  17259  setsabs  17271  setscom  17272  prdsval  17540  prdsdsval  17563  prdsdsval2  17569  prdsdsval3  17570  mreexexlem3d  17734  mreexexlem4d  17735  estrres  18227  symg2bas  19520  symgvalstruct  19524  evlseu  22299  ordtuni  23415  lfinun  23751  alexsubALTlem3  24275  ustssco  24441  trust  24455  ressprdsds  24597  xpsdsval  24607  nulmbl2  25764  uniioombllem3  25813  uniioombllem4  25814  plyeq0  26437  plyaddlem1  26439  plymullem1  26440  fta1lem  26537  vieta1lem2  26543  birthdaylem2  27189  noetasuplem2  27970  noxpordpred  28218  addsproplem1  28234  addsprop  28241  negsproplem1  28293  negsprop  28300  mulsproplemcbv  28380  mulsproplem1  28381  mulsprop  28395  precsexlemcbv  28471  precsexlem3  28474  edglnl  29600  iuninc  33034  nn0diffz0  33265  pmtrcnel2  33530  tocycval  33548  cycpmco2rn  33565  dflringlem3  33906  dflring4  33908  evlextv  34052  difelcarsg  34821  actfunsnf1o  35112  reprsuc  35123  breprexplema  35138  bnj1416  35548  mclsval  36142  mclsax  36148  rankung  36746  topjoin  36984  ttcsng  37138  ttcsntrsucg  37141  bj-tageq  37720  finixpnum  38359  poimirlem3  38372  poimirlem4  38373  poimirlem6  38375  poimirlem7  38376  poimirlem9  38378  poimirlem16  38385  poimirlem17  38386  poimirlem28  38397  mblfinlem2  38407  islshpsm  39853  lshpnel2N  39858  lkrlsp3  39977  pclfinclN  40823  dochsatshp  42324  mapfzcons1  43562  iunrelexp0  44542  isotone1  44888  fiiuncl  45899  nnsplit  46188  fourierdlem32  46967  fzopred  48211  fzopredsuc  48212  dfsclnbgr6  48774  aacllem  50772