Theorem uneq2d 4168

Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)

Hypothesis

Ref	Expression
uneq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
uneq2d	⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

Proof of Theorem uneq2d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		uneq2 4162	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956

This theorem is referenced by:  ifeq2  4530  tpeq3  4744  iununi  5099  sucprc  6460  unisucs  6461  resasplit  6778  fvun1  7000  fmptapd  7191  fndifnfp  7196  fvunsn  7199  fnsnsplit  7204  f1ofvswap  7326  oev2  8561  oarec  8600  ralxpmap  8936  sbthlem5  9127  sbthlem6  9128  domss2  9176  dif1en  9200  dif1enOLD  9202  unfi  9211  fodomfi  9350  domunfican  9361  fiint  9366  fiintOLD  9367  fodomfiOLD  9370  pm54.43  10041  kmlem2  10192  kmlem11  10201  ackbij1lem1  10259  fin23lem26  10365  axdc3lem4  10493  fpwwe2lem12  10682  wunex2  10778  wuncval2  10787  ioounsn  13517  snunico  13519  ioojoin  13523  fzsuc  13611  fseq1p1m1  13638  fseq1m1p1  13639  fzosplitsnm1  13779  fzosplitsn  13814  fzosplitpr  13815  fzosplitprm1  13816  hashfun  14476  resunimafz0  14484  s4prop  14949  fsumm1  15787  climcndslem1  15885  fprodm1  16003  ruclem4  16270  lcmfunsnlem1  16674  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  lcmfunsnlem2  16677  lcmfunsn  16681  vdwap1  17015  setscom  17217  setsidvald  17236  mreexmrid  17686  mreexexlemd  17687  mreexexlem2d  17688  cnvtsr  18633  dprd2da  20062  dmdprdsplit2lem  20065  lspun0  21009  lbsextlem4  21163  cmpcld  23410  comppfsc  23540  trfil2  23895  cldsubg  24119  tsmsres  24152  icccmplem2  24845  uniioombllem4  25621  ppiprm  27194  chtprm  27196  pntrsumbnd2  27611  noextend  27711  nodenselem5  27733  nosupbnd2lem1  27760  addsproplem1  28002  addsprop  28009  negsproplem1  28060  negsprop  28067  mulsproplemcbv  28141  mulsproplem1  28142  mulsprop  28156  precsexlemcbv  28230  precsexlem3  28233  sltonold  28283  pthdlem1  29786  wwlksnext  29913  clwwlknonex2lem1  30126  iunxunsn  32579  iunxunpr  32580  difres  32613  ofpreima2  32676  fzspl  32791  tocyc01  33138  ordtprsuni  33918  ordtcnvNEW  33919  carsgsigalem  34317  ballotlemfp1  34494  fsum2dsub  34622  reprsuc  34630  bnj941  34786  bnj944  34952  fineqvac  35111  subfacp1lem1  35184  cvmscld  35278  satf  35358  satfv1  35368  fmlasuc  35391  mrsubvrs  35527  mclsval  35568  rankaltopb  35980  rankung  36167  lindsadd  37620  lindsenlbs  37622  poimirlem1  37628  poimirlem2  37629  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem13  37640  poimirlem14  37641  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem26  37653  poimirlem28  37655  poimirlem31  37658  poimirlem32  37659  lshpnel2N  38986  paddfval  39799  hdmapval  41830  fzsplitnd  41983  lcmfunnnd  42013  metakunt24  42229  fsuppssind  42603  diophren  42824  omabs2  43345  tfsconcatrn  43355  tfsconcatrev  43361  iunrelexp0  43715  trclfvdecoml  43742  isotone1  44061  iunp1  45071  snunioo1  45525  dvmptfprodlem  45959  stoweidlem11  46026  stoweidlem26  46041  fourierdlem33  46155  fzopredsuc  47335  iccpartltu  47412  iccpartgt  47414  dfclnbgr2  47810  dfclnbgr4  47811  dfclnbgr3  47813  clnbupgr  47820  clnbgr0edg  47823  dfclnbgr5  47836  dfclnbgr6  47842  dfsclnbgr6  47844  cycl3grtri  47914  stgrclnbgr0  47932  lmod1zr  48410  tposres2  48780