Theorem uneq2d 4163

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

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

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3953

This theorem is referenced by:  ifeq2  4533  tpeq3  4748  iununi  5102  sucprc  6440  unisucs  6441  resasplit  6761  fvun1  6982  fmptapd  7171  fndifnfp  7176  fvunsn  7179  fnsnsplit  7184  f1ofvswap  7307  oev2  8529  oarec  8568  ralxpmap  8896  sbthlem5  9093  sbthlem6  9094  domss2  9142  dif1en  9166  dif1enOLD  9168  unfi  9178  domunfican  9326  fiint  9330  fodomfi  9331  pm54.43  10002  kmlem2  10152  kmlem11  10161  ackbij1lem1  10221  fin23lem26  10326  axdc3lem4  10454  fpwwe2lem12  10643  wunex2  10739  wuncval2  10748  ioounsn  13461  snunico  13463  ioojoin  13467  fzsuc  13555  fseq1p1m1  13582  fseq1m1p1  13583  fzosplitsnm1  13714  fzosplitsn  13747  fzosplitpr  13748  fzosplitprm1  13749  hashfun  14404  resunimafz0  14411  s4prop  14868  fsumm1  15704  climcndslem1  15802  fprodm1  15918  ruclem4  16184  lcmfunsnlem1  16581  lcmfunsnlem2lem1  16582  lcmfunsnlem2lem2  16583  lcmfunsnlem2  16584  lcmfunsn  16588  vdwap1  16917  setscom  17120  setsidvald  17139  setsidvaldOLD  17140  mreexmrid  17594  mreexexlemd  17595  mreexexlem2d  17596  cnvtsr  18551  dprd2da  19960  dmdprdsplit2lem  19963  lspun0  20854  lbsextlem4  21008  cmpcld  23226  comppfsc  23356  trfil2  23711  cldsubg  23935  tsmsres  23968  icccmplem2  24659  uniioombllem4  25435  ppiprm  26996  chtprm  26998  pntrsumbnd2  27413  noextend  27512  nodenselem5  27534  nosupbnd2lem1  27561  addsproplem1  27799  addsprop  27806  negsproplem1  27853  negsprop  27860  mulsproplemcbv  27928  mulsproplem1  27929  mulsprop  27943  precsexlemcbv  28017  precsexlem3  28020  sltonold  28066  pthdlem1  29456  wwlksnext  29580  clwwlknonex2lem1  29793  iunxunsn  32231  iunxunpr  32232  difres  32264  ofpreima2  32324  fzspl  32434  tocyc01  32713  ordtprsuni  33363  ordtcnvNEW  33364  carsgsigalem  33778  ballotlemfp1  33954  fsum2dsub  34083  reprsuc  34091  bnj941  34247  bnj944  34413  fineqvac  34561  subfacp1lem1  34634  cvmscld  34728  satf  34808  satfv1  34818  fmlasuc  34841  mrsubvrs  34977  mclsval  35018  rankaltopb  35421  rankung  35608  lindsadd  36945  lindsenlbs  36947  poimirlem1  36953  poimirlem2  36954  poimirlem4  36956  poimirlem6  36958  poimirlem7  36959  poimirlem8  36960  poimirlem13  36965  poimirlem14  36966  poimirlem16  36968  poimirlem17  36969  poimirlem18  36970  poimirlem19  36971  poimirlem20  36972  poimirlem21  36973  poimirlem22  36974  poimirlem26  36978  poimirlem28  36980  poimirlem31  36983  poimirlem32  36984  lshpnel2N  38319  paddfval  39132  hdmapval  41163  fzsplitnd  41315  lcmfunnnd  41344  metakunt24  41475  fsuppssind  41628  diophren  42014  omabs2  42545  tfsconcatrn  42555  tfsconcatrev  42561  iunrelexp0  42916  trclfvdecoml  42943  isotone1  43262  iunp1  44215  snunioo1  44684  dvmptfprodlem  45119  stoweidlem11  45186  stoweidlem26  45201  fourierdlem33  45315  fzopredsuc  46490  iccpartltu  46552  iccpartgt  46554  lmod1zr  47336