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 18	1 ⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∪ cun 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904

This theorem is used by:  ifeq2  4487  tpeq3  4705  iununi  5059  sucprc  6436  unisucs  6437  resasplit  6745  fvun1  6969  fmptapd  7169  fndifnfp  7174  fvunsn  7177  fnsnsplit  7182  f1ofvswap  7307  oev2  8510  oarec  8549  ralxpmap  8903  sbthlem5  9089  sbthlem6  9090  domss2  9134  dif1en  9156  unfi  9165  fodomfi  9282  domunfican  9291  fiint  9296  pm54.43  10006  kmlem2  10154  kmlem11  10163  ackbij1lem1  10221  fin23lem26  10327  axdc3lem4  10455  fpwwe2lem12  10651  wunex2  10747  wuncval2  10756  indconst1  12255  ioounsn  13530  snunico  13532  ioojoin  13536  fzsuc  13626  fseq1p1m1  13653  fseq1m1p1  13654  fzosplitsnm1  13796  fzosplitsn  13832  fzosplitpr  13833  fzosplitprm1  13834  hashfun  14502  resunimafz0  14510  s4prop  14981  fsumm1  15837  climcndslem1  15938  fprodm1  16054  ruclem4  16322  lcmfunsnlem1  16727  lcmfunsnlem2lem1  16728  lcmfunsnlem2lem2  16729  lcmfunsnlem2  16730  lcmfunsn  16734  vdwap1  17069  setscom  17272  setsidvald  17291  mreexmrid  17731  mreexexlemd  17732  mreexexlem2d  17733  cnvtsr  18676  dprd2da  20171  dmdprdsplit2lem  20174  lspun0  21195  lbsextlem4  21348  lindsenlbs  22064  cmpcld  23627  comppfsc  23758  trfil2  24113  cldsubg  24337  tsmsres  24370  icccmplem2  25050  uniioombllem4  25814  ppiprm  27387  chtprm  27389  pntrsumbnd2  27803  noextend  27902  nodenselem5  27924  nosupbnd2lem1  27951  addsproplem1  28234  addsprop  28241  negsproplem1  28293  negsprop  28300  mulsproplemcbv  28380  mulsproplem1  28381  mulsprop  28395  precsexlemcbv  28471  precsexlem3  28474  onleft  28525  ltonold  28526  oncutlt  28529  pthdlem1  30231  wwlksnext  30361  clwwlknonex2lem1  30577  iunxunsn  33039  iunxunpr  33040  difres  33073  ofpreima2  33139  fzspl  33260  tocyc01  33558  esplyind  34085  ordtprsuni  34429  ordtcnvNEW  34430  carsgsigalem  34826  ballotlemfp1  35003  fsum2dsub  35115  reprsuc  35123  bnj941  35282  bnj944  35447  fineqvac  35642  subfacp1lem1  35758  cvmscld  35852  satf  35932  satfv1  35942  fmlasuc  35965  mrsubvrs  36101  mclsval  36142  rankaltopb  36559  rankung  36746  lindsadd  38367  poimirlem1  38370  poimirlem2  38371  poimirlem4  38373  poimirlem6  38375  poimirlem7  38376  poimirlem8  38377  poimirlem13  38382  poimirlem14  38383  poimirlem16  38385  poimirlem17  38386  poimirlem18  38387  poimirlem19  38388  poimirlem20  38389  poimirlem21  38390  poimirlem22  38391  poimirlem26  38395  poimirlem28  38397  poimirlem31  38400  poimirlem32  38401  lshpnel2N  39858  paddfval  40670  hdmapval  42701  fzsplitnd  42848  lcmfunnnd  42878  fsuppssind  43439  diophren  43654  omabs2  44173  tfsconcatrn  44183  tfsconcatrev  44189  iunrelexp0  44542  trclfvdecoml  44569  isotone1  44888  iunp1  45900  snunioo1  46342  dvmptfprodlem  46772  stoweidlem11  46839  stoweidlem26  46854  fourierdlem33  46968  fzopredsuc  48212  iccpartltu  48325  iccpartgt  48327  dfclnbgr2  48739  dfclnbgr4  48740  dfclnbgr3  48742  clnbupgr  48749  clnbgr0edg  48753  dfclnbgr5  48766  dfclnbgr6  48772  dfsclnbgr6  48774  cycl3grtri  48863  stgrclnbgr0  48881  lmod1zr  49423  tposres2  49806