Theorem uneq2d 4098

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888

This theorem is referenced by:  ifeq2  4459  tpeq3  4676  iununi  5028  sucprc  6388  unisucs  6389  resasplit  6697  fvun1  6918  fmptapd  7115  fndifnfp  7120  fvunsn  7123  fnsnsplit  7128  f1ofvswap  7250  oev2  8448  oarec  8487  ralxpmap  8834  sbthlem5  9019  sbthlem6  9020  domss2  9064  dif1en  9086  unfi  9095  fodomfi  9212  domunfican  9222  fiint  9227  fodomfiOLD  9230  pm54.43  9916  kmlem2  10065  kmlem11  10074  ackbij1lem1  10132  fin23lem26  10238  axdc3lem4  10366  fpwwe2lem12  10556  wunex2  10652  wuncval2  10661  indconst1  12163  ioounsn  13421  snunico  13423  ioojoin  13427  fzsuc  13516  fseq1p1m1  13543  fseq1m1p1  13544  fzosplitsnm1  13686  fzosplitsn  13722  fzosplitpr  13723  fzosplitprm1  13724  hashfun  14390  resunimafz0  14398  s4prop  14863  fsumm1  15704  climcndslem1  15805  fprodm1  15923  ruclem4  16192  lcmfunsnlem1  16597  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  lcmfunsnlem2  16600  lcmfunsn  16604  vdwap1  16939  setscom  17141  setsidvald  17160  mreexmrid  17600  mreexexlemd  17601  mreexexlem2d  17602  cnvtsr  18545  dprd2da  20010  dmdprdsplit2lem  20013  lspun0  21001  lbsextlem4  21154  cmpcld  23385  comppfsc  23515  trfil2  23870  cldsubg  24094  tsmsres  24127  icccmplem2  24807  uniioombllem4  25571  ppiprm  27132  chtprm  27134  pntrsumbnd2  27548  noextend  27648  nodenselem5  27670  nosupbnd2lem1  27697  addsproplem1  27979  addsprop  27986  negsproplem1  28038  negsprop  28045  mulsproplemcbv  28125  mulsproplem1  28126  mulsprop  28140  precsexlemcbv  28216  precsexlem3  28219  onleft  28270  ltonold  28271  oncutlt  28274  pthdlem1  29852  wwlksnext  29979  clwwlknonex2lem1  30195  iunxunsn  32655  iunxunpr  32656  difres  32689  ofpreima2  32758  fzspl  32881  tocyc01  33199  esplyind  33759  ordtprsuni  34103  ordtcnvNEW  34104  carsgsigalem  34499  ballotlemfp1  34676  fsum2dsub  34791  reprsuc  34799  bnj941  34955  bnj944  35120  fineqvac  35297  subfacp1lem1  35407  cvmscld  35501  satf  35581  satfv1  35591  fmlasuc  35614  mrsubvrs  35750  mclsval  35791  rankaltopb  36207  rankung  36394  lindsadd  37980  lindsenlbs  37982  poimirlem1  37988  poimirlem2  37989  poimirlem4  37991  poimirlem6  37993  poimirlem7  37994  poimirlem8  37995  poimirlem13  38000  poimirlem14  38001  poimirlem16  38003  poimirlem17  38004  poimirlem18  38005  poimirlem19  38006  poimirlem20  38007  poimirlem21  38008  poimirlem22  38009  poimirlem26  38013  poimirlem28  38015  poimirlem31  38018  poimirlem32  38019  lshpnel2N  39477  paddfval  40289  hdmapval  42320  fzsplitnd  42467  lcmfunnnd  42497  fsuppssind  43043  diophren  43258  omabs2  43777  tfsconcatrn  43787  tfsconcatrev  43793  iunrelexp0  44146  trclfvdecoml  44173  isotone1  44492  iunp1  45514  snunioo1  45957  dvmptfprodlem  46387  stoweidlem11  46454  stoweidlem26  46469  fourierdlem33  46583  fzopredsuc  47787  iccpartltu  47900  iccpartgt  47902  dfclnbgr2  48314  dfclnbgr4  48315  dfclnbgr3  48317  clnbupgr  48324  clnbgr0edg  48328  dfclnbgr5  48341  dfclnbgr6  48347  dfsclnbgr6  48349  cycl3grtri  48438  stgrclnbgr0  48456  lmod1zr  48984  tposres2  49370