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 1539   ∪ cun 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893

This theorem is referenced by:  ifeq2  4465  tpeq3  4681  iununi  5029  sucprc  6345  resasplit  6653  fvun1  6868  fmptapd  7052  fndifnfp  7057  fvunsn  7060  fnsnsplit  7065  f1ofvswap  7187  oev2  8362  oarec  8402  ralxpmap  8693  sbthlem5  8883  sbthlem6  8884  domss2  8932  dif1en  8954  unfi  8964  domunfican  9096  fiint  9100  fodomfi  9101  pm54.43  9768  kmlem2  9916  kmlem11  9925  ackbij1lem1  9985  fin23lem26  10090  axdc3lem4  10218  fpwwe2lem12  10407  wunex2  10503  wuncval2  10512  ioounsn  13218  snunico  13220  ioojoin  13224  fzsuc  13312  fseq1p1m1  13339  fseq1m1p1  13340  fzosplitsnm1  13471  fzosplitsn  13504  fzosplitpr  13505  fzosplitprm1  13506  hashfun  14161  resunimafz0  14166  s4prop  14632  fsumm1  15472  climcndslem1  15570  fprodm1  15686  ruclem4  15952  lcmfunsnlem1  16351  lcmfunsnlem2lem1  16352  lcmfunsnlem2lem2  16353  lcmfunsnlem2  16354  lcmfunsn  16358  vdwap1  16687  setscom  16890  setsidvald  16909  setsidvaldOLD  16910  mreexmrid  17361  mreexexlemd  17362  mreexexlem2d  17363  cnvtsr  18315  dprd2da  19654  dmdprdsplit2lem  19657  lspun0  20282  lbsextlem4  20432  cmpcld  22562  comppfsc  22692  trfil2  23047  cldsubg  23271  tsmsres  23304  icccmplem2  23995  uniioombllem4  24759  ppiprm  26309  chtprm  26311  pntrsumbnd2  26724  pthdlem1  28143  wwlksnext  28267  clwwlknonex2lem1  28480  iunxunsn  30915  iunxunpr  30916  difres  30948  ofpreima2  31012  fzspl  31120  tocyc01  31394  ordtprsuni  31878  ordtcnvNEW  31879  carsgsigalem  32291  ballotlemfp1  32467  fsum2dsub  32596  reprsuc  32604  bnj941  32761  bnj944  32927  fineqvac  33075  subfacp1lem1  33150  cvmscld  33244  satf  33324  satfv1  33334  fmlasuc  33357  mrsubvrs  33493  mclsval  33534  noextend  33878  nodenselem5  33900  nosupbnd2lem1  33927  rankaltopb  34290  rankung  34477  lindsadd  35779  lindsenlbs  35781  poimirlem1  35787  poimirlem2  35788  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem13  35799  poimirlem14  35800  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem26  35812  poimirlem28  35814  poimirlem31  35817  poimirlem32  35818  lshpnel2N  37006  paddfval  37818  hdmapval  39849  fzsplitnd  39998  lcmfunnnd  40027  metakunt24  40155  fsuppssind  40289  diophren  40642  nlimsuc  41055  iunrelexp0  41317  trclfvdecoml  41344  isotone1  41665  iunp1  42621  snunioo1  43057  dvmptfprodlem  43492  stoweidlem11  43559  stoweidlem26  43574  fourierdlem33  43688  fzopredsuc  44826  iccpartltu  44888  iccpartgt  44890  lmod1zr  45845