Theorem uneq2d 3729

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

Syntax hints:   → wi 4   = wceq 1475   ∪ cun 3538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545

This theorem is referenced by:  ifeq2  4041  tpeq3  4223  iununi  4546  sucprc  5717  resasplit  5987  fvun1  6179  fmptapd  6342  fndifnfp  6347  fvunsn  6350  fnsnsplit  6355  oev2  7490  oarec  7529  ralxpmap  7793  sbthlem5  7959  sbthlem6  7960  domss2  8004  domunfican  8118  fiint  8122  fodomfi  8124  pm54.43  8709  kmlem2  8856  kmlem11  8865  cdaval  8875  cdaassen  8887  ackbij1lem1  8925  fin23lem26  9030  axdc3lem4  9158  fpwwe2lem13  9343  wunex2  9439  wuncval2  9448  snunico  12170  ioojoin  12174  fzsuc  12258  fseq1p1m1  12283  fseq1m1p1  12284  fzosplitsnm1  12409  fzosplitsn  12442  fzosplitprm1  12443  hashfun  13084  s4prop  13505  fsumm1  14324  climcndslem1  14420  fprodm1  14536  ruclem4  14802  lcmfunsnlem1  15188  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  lcmfunsnlem2  15191  lcmfunsn  15195  vdwap1  15519  setsidvald  15721  setscom  15731  mreexmrid  16126  mreexexlemd  16127  mreexexlem2d  16128  cnvtsr  17045  dprd2da  18264  dmdprdsplit2lem  18267  lspun0  18832  lbsextlem4  18982  cmpcld  21015  comppfsc  21145  trfil2  21501  cldsubg  21724  tsmsres  21757  icccmplem2  22434  uniioombllem4  23160  ppiprm  24677  chtprm  24679  pntrsumbnd2  25056  wwlknext  26252  eupath2lem3  26506  difres  28795  ofpreima2  28849  fzspl  28938  ordtprsuni  29293  ordtcnvNEW  29294  carsgsigalem  29704  ballotlemfp1  29880  bnj941  30097  bnj944  30262  subfacp1lem1  30415  cvmscld  30509  mrsubvrs  30673  mclsval  30714  rankaltopb  31256  rankung  31443  lindsenlbs  32574  poimirlem1  32580  poimirlem2  32581  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem13  32592  poimirlem14  32593  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem26  32605  poimirlem28  32607  poimirlem31  32610  poimirlem32  32611  lshpnel2N  33290  paddfval  34101  hdmapval  36138  diophren  36395  ioounsn  36814  iunrelexp0  37013  trclfvdecoml  37040  isotone1  37366  iunp1  38260  snunioo2  38578  snunioo1  38585  dvmptfprodlem  38834  stoweidlem11  38904  stoweidlem26  38919  fourierdlem33  39033  fzopredsuc  39946  iccpartltu  39963  iccpartgt  39965  fzosplitpr  40362  resunimafz0  40368  pthdlem1  40972  wwlksnext  41099  lmod1zr  42076