Theorem uneq2i 4145

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 4142	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)

Syntax hints:   = wceq 1540   ∪ cun 3929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936

This theorem is referenced by:  un4  4155  unundir  4157  difdif2  4276  difun2  4461  difdifdir  4472  dfif5  4522  qdass  4734  qdassr  4735  ssunpr  4815  iununi  5080  unidif0  5335  difxp1  6159  iunsuc  6444  fresaun  6754  fresaunres2  6755  fvssunirnOLD  6915  fmptap  7167  fvsnun1  7179  funiunfv  7245  onuninsuci  7840  frrlem14  8303  wfrlem13OLD  8340  wfrlem14OLD  8341  wfrlem16OLD  8343  tfrlem10  8406  oarec  8579  dfdom2  8997  fodomr  9147  fodomfir  9345  ranksuc  9884  kmlem3  10172  djuassen  10198  fin1a2lem10  10428  fin1a2lem12  10430  axdc3lem4  10472  prunioo  13503  fz0sn0fz1  13667  facnn  14298  fac0  14299  hashun3  14407  trclublem  15019  dmtrclfv  15042  fsum2dlem  15791  fsumiun  15842  incexclem  15857  fprod2dlem  16001  prmreclem4  16944  phlstr  17365  mreexexlem4d  17664  smndex1basss  18888  smndex1mgm  18890  opsrtoslem2  22019  restcld  23115  neitr  23123  fiuncmp  23347  refun0  23458  1stckgenlem  23496  filconn  23826  ufildr  23874  alexsubALTlem3  23992  ptcmplem1  23995  restmetu  24514  ovolfiniun  25459  unmbl  25495  volfiniun  25505  voliunlem1  25508  plyun0  26159  lgsquadlem3  27350  noextend  27635  noextendseq  27636  nosupbday  27674  nosupbnd1  27683  nosupbnd2  27685  noinfbday  27689  noinfbnd1  27698  noinfbnd2  27700  noetasuplem2  27703  noetasuplem3  27704  noetasuplem4  27705  noetainflem4  27709  madeun  27852  addsproplem2  27934  addsasslem1  27967  addsasslem2  27968  negsproplem2  27992  negsproplem6  27996  negsid  28004  mulsproplem2  28077  mulsproplem3  28078  mulsproplem4  28079  mulsproplem12  28087  mulsproplem13  28088  mulsproplem14  28089  mulsass  28126  precsexlemcbv  28165  onmulscl  28232  axlowdimlem3  28928  axlowdimlem17  28942  ex-un  30410  ex-pw  30415  indifundif  32510  iuninc  32546  difico  32765  esum2dlem  34128  fiunelcarsg  34353  carsgclctunlem1  34354  carsggect  34355  bnj601  34956  bnj1416  35075  subfacp1lem1  35206  cvmliftlem10  35321  satf0  35399  poimirlem4  37653  poimirlem18  37667  poimirlem21  37670  poimirlem22  37671  poimirlem25  37674  mbfresfi  37695  asindmre  37732  fsuppssind  42591  mapfzcons  42714  mapfzcons1  42715  diophin  42770  iocunico  43210  rp-fakeuninass  43515  rclexi  43614  rtrclex  43616  dfrtrcl5  43628  dfrcl2  43673  corcltrcl  43738  cotrclrcl  43741  frege109d  43756  frege131d  43763  nregmodelf1o  45015  fiiuncl  45069  cnrefiisp  45839  fourierdlem65  46180  fourierdlem89  46204  fourierdlem90  46205  fourierdlem91  46206  fourierdlem96  46211  fourierdlem97  46212  fourierdlem98  46213  fourierdlem99  46214  fourierdlem100  46215  fourierdlem105  46220  fourierdlem108  46223  fourierdlem109  46224  fourierdlem110  46225  fourierdlem112  46227  fourierdlem113  46228  isomenndlem  46539  hoidmvlelem3  46606  1fzopredsuc  47333  dfclnbgr4  47818  clnbupgr  47827  usgrexmpl2edg  48013  lmod1zr  48449  dftpos5  48829  dftpos6  48830  tposresg  48833  tposrescnv  48834  tposres3  48836