Theorem uneq2d 4093

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888

This theorem is referenced by:  ifeq2  4461  tpeq3  4677  iununi  5024  sucprc  6326  resasplit  6628  fvun1  6841  fmptapd  7025  fndifnfp  7030  fvunsn  7033  fnsnsplit  7038  f1ofvswap  7158  oev2  8315  oarec  8355  ralxpmap  8642  sbthlem5  8827  sbthlem6  8828  domss2  8872  dif1en  8907  unfi  8917  domunfican  9017  fiint  9021  fodomfi  9022  pm54.43  9690  kmlem2  9838  kmlem11  9847  ackbij1lem1  9907  fin23lem26  10012  axdc3lem4  10140  fpwwe2lem12  10329  wunex2  10425  wuncval2  10434  ioounsn  13138  snunico  13140  ioojoin  13144  fzsuc  13232  fseq1p1m1  13259  fseq1m1p1  13260  fzosplitsnm1  13390  fzosplitsn  13423  fzosplitpr  13424  fzosplitprm1  13425  hashfun  14080  resunimafz0  14085  s4prop  14551  fsumm1  15391  climcndslem1  15489  fprodm1  15605  ruclem4  15871  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  lcmfunsnlem2  16273  lcmfunsn  16277  vdwap1  16606  setscom  16809  setsidvald  16828  setsidvaldOLD  16829  mreexmrid  17269  mreexexlemd  17270  mreexexlem2d  17271  cnvtsr  18221  dprd2da  19560  dmdprdsplit2lem  19563  lspun0  20188  lbsextlem4  20338  cmpcld  22461  comppfsc  22591  trfil2  22946  cldsubg  23170  tsmsres  23203  icccmplem2  23892  uniioombllem4  24655  ppiprm  26205  chtprm  26207  pntrsumbnd2  26620  pthdlem1  28035  wwlksnext  28159  clwwlknonex2lem1  28372  iunxunsn  30807  iunxunpr  30808  difres  30840  ofpreima2  30905  fzspl  31013  tocyc01  31287  ordtprsuni  31771  ordtcnvNEW  31772  carsgsigalem  32182  ballotlemfp1  32358  fsum2dsub  32487  reprsuc  32495  bnj941  32652  bnj944  32818  fineqvac  32966  subfacp1lem1  33041  cvmscld  33135  satf  33215  satfv1  33225  fmlasuc  33248  mrsubvrs  33384  mclsval  33425  noextend  33796  nodenselem5  33818  nosupbnd2lem1  33845  rankaltopb  34208  rankung  34395  lindsadd  35697  lindsenlbs  35699  poimirlem1  35705  poimirlem2  35706  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem13  35717  poimirlem14  35718  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem26  35730  poimirlem28  35732  poimirlem31  35735  poimirlem32  35736  lshpnel2N  36926  paddfval  37738  hdmapval  39769  fzsplitnd  39919  lcmfunnnd  39948  metakunt24  40076  fsuppssind  40205  diophren  40551  iunrelexp0  41199  trclfvdecoml  41226  isotone1  41547  iunp1  42503  snunioo1  42940  dvmptfprodlem  43375  stoweidlem11  43442  stoweidlem26  43457  fourierdlem33  43571  fzopredsuc  44703  iccpartltu  44765  iccpartgt  44767  lmod1zr  45722