Theorem uneq1d 4140

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

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

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943

This theorem is referenced by:  ifeq1  4473  preq1  4671  tpeq1  4680  tpeq2  4681  tpprceq3  4739  iunxdif3  5019  iununi  5023  resasplit  6550  fresaunres2  6552  fmptpr  6936  funresdfunsn  6953  ressuppssdif  7853  sbthlem5  8633  fodomr  8670  domunfican  8793  brwdom2  9039  ackbij1lem2  9645  ttukeylem3  9935  snunioo  12867  snunioc  12869  prunioo  12870  fzpred  12958  fseq1p1m1  12984  nn0split  13025  fz0sn0fz1  13027  fzo0sn0fzo1  13129  fzosplitpr  13149  s2prop  14271  s4prop  14274  fsum1p  15110  fprod1p  15324  setsval  16515  setsabs  16528  setscom  16529  prdsval  16730  prdsdsval  16753  prdsdsval2  16759  prdsdsval3  16760  mreexexlem3d  16919  mreexexlem4d  16920  estrres  17391  symg2bas  18523  symgvalstruct  18527  evlseu  20298  ordtuni  21800  lfinun  22135  alexsubALTlem3  22659  ustssco  22825  trust  22840  ressprdsds  22983  xpsdsval  22993  nulmbl2  24139  uniioombllem3  24188  uniioombllem4  24189  plyeq0  24803  plyaddlem1  24805  plymullem1  24806  fta1lem  24898  vieta1lem2  24902  birthdaylem2  25532  edglnl  26930  iuninc  30314  pmtrcnel2  30736  tocycval  30752  cycpmco2rn  30769  difelcarsg  31570  actfunsnf1o  31877  reprsuc  31888  breprexplema  31903  bnj1416  32313  mclsval  32812  mclsax  32818  rankung  33629  topjoin  33715  bj-tageq  34290  finixpnum  34879  poimirlem3  34897  poimirlem4  34898  poimirlem6  34900  poimirlem7  34901  poimirlem9  34903  poimirlem16  34910  poimirlem17  34911  poimirlem28  34922  mblfinlem2  34932  islshpsm  36118  lshpnel2N  36123  lkrlsp3  36242  pclfinclN  37088  dochsatshp  38589  mapfzcons1  39321  iunrelexp0  40054  isotone1  40405  fiiuncl  41334  nnsplit  41633  fourierdlem32  42431  fzopred  43529  fzopredsuc  43530  aacllem  44909