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  6746  fvun1  6970  fmptapd  7170  fndifnfp  7175  fvunsn  7178  fnsnsplit  7183  f1ofvswap  7308  oev2  8511  oarec  8550  ralxpmap  8904  sbthlem5  9090  sbthlem6  9091  domss2  9135  dif1en  9157  unfi  9166  fodomfi  9283  domunfican  9292  fiint  9297  pm54.43  10007  kmlem2  10155  kmlem11  10164  ackbij1lem1  10222  fin23lem26  10328  axdc3lem4  10456  fpwwe2lem12  10652  wunex2  10748  wuncval2  10757  indconst1  12256  ioounsn  13531  snunico  13533  ioojoin  13537  fzsuc  13627  fseq1p1m1  13654  fseq1m1p1  13655  fzosplitsnm1  13797  fzosplitsn  13833  fzosplitpr  13834  fzosplitprm1  13835  hashfun  14503  resunimafz0  14511  s4prop  14982  fsumm1  15838  climcndslem1  15939  fprodm1  16055  ruclem4  16323  lcmfunsnlem1  16728  lcmfunsnlem2lem1  16729  lcmfunsnlem2lem2  16730  lcmfunsnlem2  16731  lcmfunsn  16735  vdwap1  17070  setscom  17273  setsidvald  17292  mreexmrid  17732  mreexexlemd  17733  mreexexlem2d  17734  cnvtsr  18677  dprd2da  20172  dmdprdsplit2lem  20175  lspun0  21196  lbsextlem4  21349  lindsenlbs  22065  cmpcld  23628  comppfsc  23759  trfil2  24114  cldsubg  24338  tsmsres  24371  icccmplem2  25051  uniioombllem4  25815  ppiprm  27388  chtprm  27390  pntrsumbnd2  27804  noextend  27903  nodenselem5  27925  nosupbnd2lem1  27952  addsproplem1  28235  addsprop  28242  negsproplem1  28294  negsprop  28301  mulsproplemcbv  28381  mulsproplem1  28382  mulsprop  28396  precsexlemcbv  28472  precsexlem3  28475  onleft  28526  ltonold  28527  oncutlt  28530  pthdlem1  30232  wwlksnext  30362  clwwlknonex2lem1  30578  iunxunsn  33040  iunxunpr  33041  difres  33074  ofpreima2  33140  fzspl  33261  tocyc01  33559  esplyind  34086  ordtprsuni  34430  ordtcnvNEW  34431  carsgsigalem  34827  ballotlemfp1  35004  fsum2dsub  35116  reprsuc  35124  bnj941  35283  bnj944  35448  fineqvac  35643  subfacp1lem1  35759  cvmscld  35853  satf  35933  satfv1  35943  fmlasuc  35966  mrsubvrs  36102  mclsval  36143  rankaltopb  36560  rankung  36747  lindsadd  38368  poimirlem1  38371  poimirlem2  38372  poimirlem4  38374  poimirlem6  38376  poimirlem7  38377  poimirlem8  38378  poimirlem13  38383  poimirlem14  38384  poimirlem16  38386  poimirlem17  38387  poimirlem18  38388  poimirlem19  38389  poimirlem20  38390  poimirlem21  38391  poimirlem22  38392  poimirlem26  38396  poimirlem28  38398  poimirlem31  38401  poimirlem32  38402  lshpnel2N  39859  paddfval  40671  hdmapval  42702  fzsplitnd  42849  lcmfunnnd  42879  fsuppssind  43440  diophren  43655  omabs2  44174  tfsconcatrn  44184  tfsconcatrev  44190  iunrelexp0  44543  trclfvdecoml  44570  isotone1  44889  iunp1  45901  snunioo1  46343  dvmptfprodlem  46773  stoweidlem11  46840  stoweidlem26  46855  fourierdlem33  46969  fzopredsuc  48213  iccpartltu  48326  iccpartgt  48328  dfclnbgr2  48740  dfclnbgr4  48741  dfclnbgr3  48743  clnbupgr  48750  clnbgr0edg  48754  dfclnbgr5  48767  dfclnbgr6  48773  dfsclnbgr6  48775  cycl3grtri  48864  stgrclnbgr0  48882  lmod1zr  49424  tposres2  49807