Theorem uneq1d 4112

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

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3895

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902

This theorem is referenced by:  ifeq1  4474  preq1  4681  tpeq1  4690  tpeq2  4691  tpprceq3  4751  iunxdif3  5038  iununi  5042  resasplit  6688  fresaunres2  6690  fmptpr  7101  funresdfunsn  7118  ressuppssdif  8110  on2recsov  8578  sbthlem5  8999  fodomr  9036  domunfican  9201  fodomfir  9207  brwdom2  9454  ackbij1lem2  10106  ttukeylem3  10397  snunioo  13373  snunioc  13375  prunioo  13376  fzpred  13467  fseq1p1m1  13493  nn0split  13538  fz0sn0fz1  13540  fzo0sn0fzo1  13650  fzosplitpr  13672  s2prop  14809  s4prop  14812  fsum1p  15655  fprod1p  15870  setsval  17073  setsabs  17085  setscom  17086  prdsval  17354  prdsdsval  17377  prdsdsval2  17383  prdsdsval3  17384  mreexexlem3d  17547  mreexexlem4d  17548  estrres  18040  symg2bas  19300  symgvalstruct  19304  evlseu  22013  ordtuni  23100  lfinun  23435  alexsubALTlem3  23959  ustssco  24125  trust  24139  ressprdsds  24281  xpsdsval  24291  nulmbl2  25459  uniioombllem3  25508  uniioombllem4  25509  plyeq0  26138  plyaddlem1  26140  plymullem1  26141  fta1lem  26237  vieta1lem2  26241  birthdaylem2  26884  noetasuplem2  27668  noxpordpred  27891  addsproplem1  27907  addsprop  27914  negsproplem1  27965  negsprop  27972  mulsproplemcbv  28049  mulsproplem1  28050  mulsprop  28064  precsexlemcbv  28139  precsexlem3  28142  edglnl  29116  iuninc  32532  pmtrcnel2  33051  tocycval  33069  cycpmco2rn  33086  difelcarsg  34315  actfunsnf1o  34609  reprsuc  34620  breprexplema  34635  bnj1416  35043  mclsval  35599  mclsax  35605  rankung  36200  topjoin  36399  bj-tageq  37010  finixpnum  37645  poimirlem3  37663  poimirlem4  37664  poimirlem6  37666  poimirlem7  37667  poimirlem9  37669  poimirlem16  37676  poimirlem17  37677  poimirlem28  37688  mblfinlem2  37698  islshpsm  39019  lshpnel2N  39024  lkrlsp3  39143  pclfinclN  39989  dochsatshp  41490  mapfzcons1  42750  iunrelexp0  43735  isotone1  44081  fiiuncl  45102  nnsplit  45397  fourierdlem32  46177  fzopred  47353  fzopredsuc  47354  dfsclnbgr6  47889  aacllem  49833