Theorem uneq2i 4163

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

This proof depends on syntax axioms:   = wceq 1569   ∪ cun 4148

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4150

This theorem is used by:  un4  4172  unundir  4174  difdif2  4240  difun2  4436  difdifdir  4446  dfif5  4498  qdass  4710  qdassr  4711  ssunpr  4788  iununi  5058  unidif0  5321  unidif0OLD  5322  difxp1  6158  iunsuc  6453  fresaun  6758  fresaunres2  6759  fmptap  7179  fvsnun1  7191  funiunfv  7256  onuninsuci  7855  frrlem14  8325  tfrlem10  8403  oarec  8578  dfdom2  9013  fodomr  9155  fodomfir  9327  ranksuc  9889  kmlem3  10238  djuassen  10264  fin1a2lem10  10494  fin1a2lem12  10496  axdc3lem4  10538  prunioo  13619  fz0sn0fz1  13786  facnn  14426  fac0  14427  hashun3  14535  trclublem  15157  dmtrclfv  15180  fsum2dlem  15945  fsumiun  15997  incexclem  16014  fprod2dlem  16156  prmreclem4  17106  phlstr  17526  mreexexlem4d  17830  smndex1basss  19113  smndex1mgm  19115  opsrtoslem2  22374  restcld  23499  neitr  23507  fiuncmp  23731  refun0  23843  1stckgenlem  23881  filconn  24211  ufildr  24259  alexsubALTlem3  24377  ptcmplem1  24380  restmetu  24898  ovolfiniun  25831  unmbl  25867  volfiniun  25877  voliunlem1  25880  plyun0  26524  lgsquadlem3  27718  noextend  28032  noextendseq  28033  nosupbday  28071  nosupbnd1  28080  nosupbnd2  28082  noinfbday  28086  noinfbnd1  28095  noinfbnd2  28097  noetasuplem2  28100  noetasuplem3  28101  noetasuplem4  28102  noetainflem4  28106  madeun  28279  addsproplem2  28365  addsasslem1  28398  addsasslem2  28399  negsproplem2  28424  negsproplem6  28428  negsid  28436  mulsproplem2  28512  mulsproplem3  28513  mulsproplem4  28514  mulsproplem12  28522  mulsproplem13  28523  mulsproplem14  28524  mulsass  28561  precsexlemcbv  28601  onmulscl  28673  axlowdimlem3  29531  axlowdimlem17  29545  ex-un  31034  ex-pw  31039  indifundif  33171  iuninc  33206  difico  33425  esum2dlem  34774  fiunelcarsg  34998  carsgclctunlem1  34999  carsggect  35000  bnj601  35600  bnj1416  35719  subfacp1lem1  36062  cvmliftlem10  36177  satf0  36255  poimirlem4  38679  poimirlem18  38693  poimirlem21  38696  poimirlem22  38697  poimirlem25  38700  mbfresfi  38721  asindmre  38758  dmuncnvepres  39460  blockadjliftmap  39527  fsuppssind  43758  mapfzcons  43864  mapfzcons1  43865  diophin  43920  iocunico  44350  rp-fakeuninass  44654  rclexi  44752  rtrclex  44754  dfrtrcl5  44766  dfrcl2  44811  corcltrcl  44876  cotrclrcl  44879  frege109d  44894  frege131d  44901  nregmodelf1o  46141  fiiuncl  46218  cnrefiisp  46976  fourierdlem65  47317  fourierdlem89  47341  fourierdlem90  47342  fourierdlem91  47343  fourierdlem96  47348  fourierdlem97  47349  fourierdlem98  47350  fourierdlem99  47351  fourierdlem100  47352  fourierdlem105  47357  fourierdlem108  47360  fourierdlem109  47361  fourierdlem110  47362  fourierdlem112  47364  fourierdlem113  47365  isomenndlem  47676  hoidmvlelem3  47743  1fzopredsuc  48531  dfclnbgr4  49058  clnbupgr  49067  usgrexmpl2edg  49263  lmod1zr  49741  dftpos5  50123  dftpos6  50124  tposresg  50127  tposrescnv  50128  tposres3  50130