Theorem uneq1d 4096

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

Syntax hints:   → wi 4   = wceq 1539   ∪ cun 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892

This theorem is referenced by:  ifeq1  4463  preq1  4669  tpeq1  4678  tpeq2  4679  tpprceq3  4737  iunxdif3  5024  iununi  5028  resasplit  6644  fresaunres2  6646  fmptpr  7044  funresdfunsn  7061  ressuppssdif  8001  sbthlem5  8874  fodomr  8915  domunfican  9087  brwdom2  9332  ackbij1lem2  9977  ttukeylem3  10267  snunioo  13210  snunioc  13212  prunioo  13213  fzpred  13304  fseq1p1m1  13330  nn0split  13371  fz0sn0fz1  13373  fzo0sn0fzo1  13476  fzosplitpr  13496  s2prop  14620  s4prop  14623  fsum1p  15465  fprod1p  15678  setsval  16868  setsabs  16880  setscom  16881  prdsval  17166  prdsdsval  17189  prdsdsval2  17195  prdsdsval3  17196  mreexexlem3d  17355  mreexexlem4d  17356  estrres  17856  symg2bas  19000  symgvalstruct  19004  symgvalstructOLD  19005  evlseu  21293  ordtuni  22341  lfinun  22676  alexsubALTlem3  23200  ustssco  23366  trust  23381  ressprdsds  23524  xpsdsval  23534  nulmbl2  24700  uniioombllem3  24749  uniioombllem4  24750  plyeq0  25372  plyaddlem1  25374  plymullem1  25375  fta1lem  25467  vieta1lem2  25471  birthdaylem2  26102  edglnl  27513  iuninc  30900  pmtrcnel2  31359  tocycval  31375  cycpmco2rn  31392  difelcarsg  32277  actfunsnf1o  32584  reprsuc  32595  breprexplema  32610  bnj1416  33019  mclsval  33525  mclsax  33531  on2recsov  33827  noetasuplem2  33937  noxpordpred  34110  rankung  34468  topjoin  34554  bj-tageq  35166  finixpnum  35762  poimirlem3  35780  poimirlem4  35781  poimirlem6  35783  poimirlem7  35784  poimirlem9  35786  poimirlem16  35793  poimirlem17  35794  poimirlem28  35805  mblfinlem2  35815  islshpsm  36994  lshpnel2N  36999  lkrlsp3  37118  pclfinclN  37964  dochsatshp  39465  metakunt24  40148  mapfzcons1  40539  iunrelexp0  41310  isotone1  41658  fiiuncl  42613  nnsplit  42897  fourierdlem32  43680  fzopred  44814  fzopredsuc  44815  aacllem  46505