Theorem uneq2d 4117

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

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

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 2115  ax-9 2123  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903

This theorem is referenced by:  ifeq2  4481  tpeq3  4698  iununi  5051  sucprc  6392  unisucs  6393  resasplit  6701  fvun1  6922  fmptapd  7114  fndifnfp  7119  fvunsn  7122  fnsnsplit  7127  f1ofvswap  7249  oev2  8447  oarec  8486  ralxpmap  8830  sbthlem5  9015  sbthlem6  9016  domss2  9060  dif1en  9082  unfi  9091  fodomfi  9207  domunfican  9217  fiint  9222  fodomfiOLD  9225  pm54.43  9905  kmlem2  10054  kmlem11  10063  ackbij1lem1  10121  fin23lem26  10227  axdc3lem4  10355  fpwwe2lem12  10544  wunex2  10640  wuncval2  10649  ioounsn  13384  snunico  13386  ioojoin  13390  fzsuc  13478  fseq1p1m1  13505  fseq1m1p1  13506  fzosplitsnm1  13647  fzosplitsn  13683  fzosplitpr  13684  fzosplitprm1  13685  hashfun  14351  resunimafz0  14359  s4prop  14824  fsumm1  15665  climcndslem1  15763  fprodm1  15881  ruclem4  16150  lcmfunsnlem1  16555  lcmfunsnlem2lem1  16556  lcmfunsnlem2lem2  16557  lcmfunsnlem2  16558  lcmfunsn  16562  vdwap1  16896  setscom  17098  setsidvald  17117  mreexmrid  17557  mreexexlemd  17558  mreexexlem2d  17559  cnvtsr  18502  dprd2da  19964  dmdprdsplit2lem  19967  lspun0  20953  lbsextlem4  21107  cmpcld  23337  comppfsc  23467  trfil2  23822  cldsubg  24046  tsmsres  24079  icccmplem2  24759  uniioombllem4  25534  ppiprm  27108  chtprm  27110  pntrsumbnd2  27525  noextend  27625  nodenselem5  27647  nosupbnd2lem1  27674  addsproplem1  27932  addsprop  27939  negsproplem1  27990  negsprop  27997  mulsproplemcbv  28074  mulsproplem1  28075  mulsprop  28089  precsexlemcbv  28164  precsexlem3  28167  onsleft  28217  sltonold  28218  onscutlt  28221  pthdlem1  29765  wwlksnext  29892  clwwlknonex2lem1  30108  iunxunsn  32567  iunxunpr  32568  difres  32601  ofpreima2  32670  fzspl  32797  indconst1  32868  tocyc01  33128  esplyind  33659  ordtprsuni  34004  ordtcnvNEW  34005  carsgsigalem  34400  ballotlemfp1  34577  fsum2dsub  34692  reprsuc  34700  bnj941  34856  bnj944  35022  fineqvac  35211  subfacp1lem1  35295  cvmscld  35389  satf  35469  satfv1  35479  fmlasuc  35502  mrsubvrs  35638  mclsval  35679  rankaltopb  36095  rankung  36282  lindsadd  37726  lindsenlbs  37728  poimirlem1  37734  poimirlem2  37735  poimirlem4  37737  poimirlem6  37739  poimirlem7  37740  poimirlem8  37741  poimirlem13  37746  poimirlem14  37747  poimirlem16  37749  poimirlem17  37750  poimirlem18  37751  poimirlem19  37752  poimirlem20  37753  poimirlem21  37754  poimirlem22  37755  poimirlem26  37759  poimirlem28  37761  poimirlem31  37764  poimirlem32  37765  lshpnel2N  39157  paddfval  39969  hdmapval  42000  fzsplitnd  42148  lcmfunnnd  42178  fsuppssind  42751  diophren  42970  omabs2  43489  tfsconcatrn  43499  tfsconcatrev  43505  iunrelexp0  43859  trclfvdecoml  43886  isotone1  44205  iunp1  45227  snunioo1  45674  dvmptfprodlem  46104  stoweidlem11  46171  stoweidlem26  46186  fourierdlem33  46300  fzopredsuc  47485  iccpartltu  47587  iccpartgt  47589  dfclnbgr2  47985  dfclnbgr4  47986  dfclnbgr3  47988  clnbupgr  47995  clnbgr0edg  47999  dfclnbgr5  48012  dfclnbgr6  48018  dfsclnbgr6  48020  cycl3grtri  48109  stgrclnbgr0  48127  lmod1zr  48655  tposres2  49041