Theorem uneq2d 4163

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

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

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953

This theorem is referenced by:  ifeq2  4533  tpeq3  4748  iununi  5102  sucprc  6440  unisucs  6441  resasplit  6761  fvun1  6982  fmptapd  7168  fndifnfp  7173  fvunsn  7176  fnsnsplit  7181  f1ofvswap  7303  oev2  8522  oarec  8561  ralxpmap  8889  sbthlem5  9086  sbthlem6  9087  domss2  9135  dif1en  9159  dif1enOLD  9161  unfi  9171  domunfican  9319  fiint  9323  fodomfi  9324  pm54.43  9995  kmlem2  10145  kmlem11  10154  ackbij1lem1  10214  fin23lem26  10319  axdc3lem4  10447  fpwwe2lem12  10636  wunex2  10732  wuncval2  10741  ioounsn  13453  snunico  13455  ioojoin  13459  fzsuc  13547  fseq1p1m1  13574  fseq1m1p1  13575  fzosplitsnm1  13706  fzosplitsn  13739  fzosplitpr  13740  fzosplitprm1  13741  hashfun  14396  resunimafz0  14403  s4prop  14860  fsumm1  15696  climcndslem1  15794  fprodm1  15910  ruclem4  16176  lcmfunsnlem1  16573  lcmfunsnlem2lem1  16574  lcmfunsnlem2lem2  16575  lcmfunsnlem2  16576  lcmfunsn  16580  vdwap1  16909  setscom  17112  setsidvald  17131  setsidvaldOLD  17132  mreexmrid  17586  mreexexlemd  17587  mreexexlem2d  17588  cnvtsr  18540  dprd2da  19911  dmdprdsplit2lem  19914  lspun0  20621  lbsextlem4  20773  cmpcld  22905  comppfsc  23035  trfil2  23390  cldsubg  23614  tsmsres  23647  icccmplem2  24338  uniioombllem4  25102  ppiprm  26652  chtprm  26654  pntrsumbnd2  27067  noextend  27166  nodenselem5  27188  nosupbnd2lem1  27215  addsproplem1  27450  addsprop  27457  negsproplem1  27499  negsprop  27506  mulsproplemcbv  27568  mulsproplem1  27569  mulsprop  27583  precsexlemcbv  27649  precsexlem3  27652  pthdlem1  29020  wwlksnext  29144  clwwlknonex2lem1  29357  iunxunsn  31793  iunxunpr  31794  difres  31826  ofpreima2  31886  fzspl  31996  tocyc01  32272  ordtprsuni  32894  ordtcnvNEW  32895  carsgsigalem  33309  ballotlemfp1  33485  fsum2dsub  33614  reprsuc  33622  bnj941  33778  bnj944  33944  fineqvac  34092  subfacp1lem1  34165  cvmscld  34259  satf  34339  satfv1  34349  fmlasuc  34372  mrsubvrs  34508  mclsval  34549  rankaltopb  34946  rankung  35133  lindsadd  36476  lindsenlbs  36478  poimirlem1  36484  poimirlem2  36485  poimirlem4  36487  poimirlem6  36489  poimirlem7  36490  poimirlem8  36491  poimirlem13  36496  poimirlem14  36497  poimirlem16  36499  poimirlem17  36500  poimirlem18  36501  poimirlem19  36502  poimirlem20  36503  poimirlem21  36504  poimirlem22  36505  poimirlem26  36509  poimirlem28  36511  poimirlem31  36514  poimirlem32  36515  lshpnel2N  37850  paddfval  38663  hdmapval  40694  fzsplitnd  40843  lcmfunnnd  40872  metakunt24  41003  fsuppssind  41167  diophren  41541  omabs2  42072  tfsconcatrn  42082  tfsconcatrev  42088  iunrelexp0  42443  trclfvdecoml  42470  isotone1  42789  iunp1  43743  snunioo1  44215  dvmptfprodlem  44650  stoweidlem11  44717  stoweidlem26  44732  fourierdlem33  44846  fzopredsuc  46021  iccpartltu  46083  iccpartgt  46085  lmod1zr  47164