Theorem uneq2d 3990

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

Syntax hints:   → wi 4   = wceq 1601   ∪ cun 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-un 3797

This theorem is referenced by:  ifeq2  4312  tpeq3  4511  iununi  4846  sucprc  6053  resasplit  6326  fvun1  6531  fmptapd  6706  fndifnfp  6711  fvunsn  6714  fnsnsplit  6723  oev2  7889  oarec  7928  ralxpmap  8195  sbthlem5  8364  sbthlem6  8365  domss2  8409  domunfican  8523  fiint  8527  fodomfi  8529  pm54.43  9161  kmlem2  9310  kmlem11  9319  cdaval  9329  cdaassen  9341  ackbij1lem1  9379  fin23lem26  9484  axdc3lem4  9612  fpwwe2lem13  9801  wunex2  9897  wuncval2  9906  ioounsn  12618  ioounsnOLD  12619  snunico  12621  ioojoin  12625  fzsuc  12710  fseq1p1m1  12737  fseq1m1p1  12738  fzosplitsnm1  12867  fzosplitsn  12900  fzosplitpr  12901  fzosplitprm1  12902  hashfun  13544  resunimafz0  13549  s4prop  14067  fsumm1  14896  climcndslem1  14994  fprodm1  15109  ruclem4  15376  lcmfunsnlem1  15766  lcmfunsnlem2lem1  15767  lcmfunsnlem2lem2  15768  lcmfunsnlem2  15769  lcmfunsn  15773  vdwap1  16096  setsidvald  16297  setscom  16310  mreexmrid  16700  mreexexlemd  16701  mreexexlem2d  16702  cnvtsr  17619  dprd2da  18839  dmdprdsplit2lem  18842  lspun0  19417  lbsextlem4  19569  cmpcld  21625  comppfsc  21755  trfil2  22110  cldsubg  22333  tsmsres  22366  icccmplem2  23045  uniioombllem4  23801  ppiprm  25340  chtprm  25342  pntrsumbnd2  25725  pthdlem1  27135  wwlksnext  27271  clwwlknonex2lem1  27526  difres  29993  ofpreima2  30048  fzspl  30128  ordtprsuni  30571  ordtcnvNEW  30572  carsgsigalem  30983  ballotlemfp1  31160  fsum2dsub  31295  reprsuc  31303  bnj941  31450  bnj944  31615  subfacp1lem1  31768  cvmscld  31862  mrsubvrs  32026  mclsval  32067  noextend  32416  nodenselem5  32435  nosupbnd2lem1  32458  rankaltopb  32683  rankung  32870  lindsadd  34037  lindsenlbs  34039  poimirlem1  34045  poimirlem2  34046  poimirlem4  34048  poimirlem6  34050  poimirlem7  34051  poimirlem8  34052  poimirlem13  34057  poimirlem14  34058  poimirlem16  34060  poimirlem17  34061  poimirlem18  34062  poimirlem19  34063  poimirlem20  34064  poimirlem21  34065  poimirlem22  34066  poimirlem26  34070  poimirlem28  34072  poimirlem31  34075  poimirlem32  34076  lshpnel2N  35148  paddfval  35960  hdmapval  37991  diophren  38351  iunrelexp0  38965  trclfvdecoml  38992  isotone1  39316  iunp1  40180  snunioo1  40661  dvmptfprodlem  41101  stoweidlem11  41169  stoweidlem26  41184  fourierdlem33  41298  fzopredsuc  42379  iccpartltu  42407  iccpartgt  42409  lmod1zr  43311