Theorem uneq2i 4160

Description: Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
uneq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
uneq2i	⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)

Proof of Theorem uneq2i

Step	Hyp	Ref	Expression
1		uneq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		uneq2 4157	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)

Syntax hints:   = wceq 1542   ∪ cun 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3953

This theorem is referenced by:  un4  4169  unundir  4171  difdif2  4286  difun2  4480  difdifdir  4491  dfif5  4544  qdass  4757  qdassr  4758  ssunpr  4835  iununi  5102  unidif0  5358  difxp1  6162  iunsuc  6447  fresaun  6760  fresaunres2  6761  fvssunirnOLD  6923  fmptap  7165  fvsnun1  7177  funiunfv  7244  onuninsuci  7826  frrlem14  8281  wfrlem13OLD  8318  wfrlem14OLD  8319  wfrlem16OLD  8321  tfrlem10  8384  oarec  8559  dfdom2  8971  fodomr  9125  ranksuc  9857  kmlem3  10144  djuassen  10170  fin1a2lem10  10401  fin1a2lem12  10403  axdc3lem4  10445  prunioo  13455  fz0sn0fz1  13615  facnn  14232  fac0  14233  hashun3  14341  trclublem  14939  dmtrclfv  14962  fsum2dlem  15713  fsumiun  15764  incexclem  15779  fprod2dlem  15921  prmreclem4  16849  phlstr  17288  mreexexlem4d  17588  smndex1basss  18783  smndex1mgm  18785  opsrtoslem2  21609  restcld  22668  neitr  22676  fiuncmp  22900  refun0  23011  1stckgenlem  23049  filconn  23379  ufildr  23427  alexsubALTlem3  23545  ptcmplem1  23548  restmetu  24071  ovolfiniun  25010  unmbl  25046  volfiniun  25056  voliunlem1  25059  plyun0  25703  lgsquadlem3  26875  noextend  27159  noextendseq  27160  nosupbday  27198  nosupbnd1  27207  nosupbnd2  27209  noinfbday  27213  noinfbnd1  27222  noinfbnd2  27224  noetasuplem2  27227  noetasuplem3  27228  noetasuplem4  27229  noetainflem4  27233  madeun  27368  addsproplem2  27444  addsasslem1  27476  addsasslem2  27477  negsproplem2  27493  negsproplem6  27497  negsid  27505  mulsproplem2  27563  mulsproplem3  27564  mulsproplem4  27565  mulsproplem12  27573  mulsproplem13  27574  mulsproplem14  27575  mulsass  27611  precsexlemcbv  27642  axlowdimlem3  28192  axlowdimlem17  28206  ex-un  29667  ex-pw  29672  indifundif  31750  iuninc  31780  difico  31982  esum2dlem  33079  fiunelcarsg  33304  carsgclctunlem1  33305  carsggect  33306  bnj601  33920  bnj1416  34039  subfacp1lem1  34159  cvmliftlem10  34274  satf0  34352  poimirlem4  36481  poimirlem18  36495  poimirlem21  36498  poimirlem22  36499  poimirlem25  36502  mbfresfi  36523  asindmre  36560  fsuppssind  41163  mapfzcons  41440  mapfzcons1  41441  diophin  41496  iocunico  41946  rp-fakeuninass  42253  rclexi  42352  rtrclex  42354  dfrtrcl5  42366  dfrcl2  42411  corcltrcl  42476  cotrclrcl  42479  frege109d  42494  frege131d  42501  fiiuncl  43738  cnrefiisp  44533  fourierdlem65  44874  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  fourierdlem96  44905  fourierdlem97  44906  fourierdlem98  44907  fourierdlem99  44908  fourierdlem100  44909  fourierdlem105  44914  fourierdlem108  44917  fourierdlem109  44918  fourierdlem110  44919  fourierdlem112  44921  fourierdlem113  44922  isomenndlem  45233  hoidmvlelem3  45300  1fzopredsuc  46019  lmod1zr  47128