Theorem uneq2d 4115

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3435  df-un 3904

This theorem is referenced by:  ifeq2  4477  tpeq3  4694  iununi  5044  sucprc  6379  unisucs  6380  resasplit  6688  fvun1  6907  fmptapd  7099  fndifnfp  7104  fvunsn  7107  fnsnsplit  7112  f1ofvswap  7234  oev2  8432  oarec  8471  ralxpmap  8814  sbthlem5  8998  sbthlem6  8999  domss2  9043  dif1en  9065  unfi  9074  fodomfi  9190  domunfican  9200  fiint  9205  fodomfiOLD  9208  pm54.43  9885  kmlem2  10034  kmlem11  10043  ackbij1lem1  10101  fin23lem26  10207  axdc3lem4  10335  fpwwe2lem12  10524  wunex2  10620  wuncval2  10629  ioounsn  13368  snunico  13370  ioojoin  13374  fzsuc  13462  fseq1p1m1  13489  fseq1m1p1  13490  fzosplitsnm1  13631  fzosplitsn  13666  fzosplitpr  13667  fzosplitprm1  13668  hashfun  14332  resunimafz0  14340  s4prop  14804  fsumm1  15645  climcndslem1  15743  fprodm1  15861  ruclem4  16130  lcmfunsnlem1  16535  lcmfunsnlem2lem1  16536  lcmfunsnlem2lem2  16537  lcmfunsnlem2  16538  lcmfunsn  16542  vdwap1  16876  setscom  17078  setsidvald  17097  mreexmrid  17536  mreexexlemd  17537  mreexexlem2d  17538  cnvtsr  18481  dprd2da  19910  dmdprdsplit2lem  19913  lspun0  20898  lbsextlem4  21052  cmpcld  23271  comppfsc  23401  trfil2  23756  cldsubg  23980  tsmsres  24013  icccmplem2  24693  uniioombllem4  25468  ppiprm  27042  chtprm  27044  pntrsumbnd2  27459  noextend  27559  nodenselem5  27581  nosupbnd2lem1  27608  addsproplem1  27866  addsprop  27873  negsproplem1  27924  negsprop  27931  mulsproplemcbv  28008  mulsproplem1  28009  mulsprop  28023  precsexlemcbv  28098  precsexlem3  28101  onsleft  28151  sltonold  28152  onscutlt  28155  pthdlem1  29698  wwlksnext  29825  clwwlknonex2lem1  30038  iunxunsn  32498  iunxunpr  32499  difres  32532  ofpreima2  32600  fzspl  32724  tocyc01  33055  ordtprsuni  33900  ordtcnvNEW  33901  carsgsigalem  34296  ballotlemfp1  34473  fsum2dsub  34588  reprsuc  34596  bnj941  34752  bnj944  34918  fineqvac  35085  subfacp1lem1  35169  cvmscld  35263  satf  35343  satfv1  35353  fmlasuc  35376  mrsubvrs  35512  mclsval  35553  rankaltopb  35970  rankung  36157  lindsadd  37610  lindsenlbs  37612  poimirlem1  37618  poimirlem2  37619  poimirlem4  37621  poimirlem6  37623  poimirlem7  37624  poimirlem8  37625  poimirlem13  37630  poimirlem14  37631  poimirlem16  37633  poimirlem17  37634  poimirlem18  37635  poimirlem19  37636  poimirlem20  37637  poimirlem21  37638  poimirlem22  37639  poimirlem26  37643  poimirlem28  37645  poimirlem31  37648  poimirlem32  37649  lshpnel2N  38981  paddfval  39793  hdmapval  41824  fzsplitnd  41972  lcmfunnnd  42002  fsuppssind  42583  diophren  42803  omabs2  43322  tfsconcatrn  43332  tfsconcatrev  43338  iunrelexp0  43692  trclfvdecoml  43719  isotone1  44038  iunp1  45060  snunioo1  45509  dvmptfprodlem  45939  stoweidlem11  46006  stoweidlem26  46021  fourierdlem33  46135  fzopredsuc  47321  iccpartltu  47423  iccpartgt  47425  dfclnbgr2  47821  dfclnbgr4  47822  dfclnbgr3  47824  clnbupgr  47831  clnbgr0edg  47835  dfclnbgr5  47848  dfclnbgr6  47854  dfsclnbgr6  47856  cycl3grtri  47945  stgrclnbgr0  47963  lmod1zr  48492  tposres2  48878