Theorem uneq2i 4161

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

Syntax hints:   = wceq 1542   ∪ cun 3947

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 3954

This theorem is referenced by:  un4  4170  unundir  4172  difdif2  4287  difun2  4481  difdifdir  4492  dfif5  4545  qdass  4758  qdassr  4759  ssunpr  4836  iununi  5103  unidif0  5359  difxp1  6165  iunsuc  6450  fresaun  6763  fresaunres2  6764  fvssunirnOLD  6926  fmptap  7168  fvsnun1  7180  funiunfv  7247  onuninsuci  7829  frrlem14  8284  wfrlem13OLD  8321  wfrlem14OLD  8322  wfrlem16OLD  8324  tfrlem10  8387  oarec  8562  dfdom2  8974  fodomr  9128  ranksuc  9860  kmlem3  10147  djuassen  10173  fin1a2lem10  10404  fin1a2lem12  10406  axdc3lem4  10448  prunioo  13458  fz0sn0fz1  13618  facnn  14235  fac0  14236  hashun3  14344  trclublem  14942  dmtrclfv  14965  fsum2dlem  15716  fsumiun  15767  incexclem  15782  fprod2dlem  15924  prmreclem4  16852  phlstr  17291  mreexexlem4d  17591  smndex1basss  18786  smndex1mgm  18788  opsrtoslem2  21617  restcld  22676  neitr  22684  fiuncmp  22908  refun0  23019  1stckgenlem  23057  filconn  23387  ufildr  23435  alexsubALTlem3  23553  ptcmplem1  23556  restmetu  24079  ovolfiniun  25018  unmbl  25054  volfiniun  25064  voliunlem1  25067  plyun0  25711  lgsquadlem3  26885  noextend  27169  noextendseq  27170  nosupbday  27208  nosupbnd1  27217  nosupbnd2  27219  noinfbday  27223  noinfbnd1  27232  noinfbnd2  27234  noetasuplem2  27237  noetasuplem3  27238  noetasuplem4  27239  noetainflem4  27243  madeun  27378  addsproplem2  27454  addsasslem1  27486  addsasslem2  27487  negsproplem2  27503  negsproplem6  27507  negsid  27515  mulsproplem2  27573  mulsproplem3  27574  mulsproplem4  27575  mulsproplem12  27583  mulsproplem13  27584  mulsproplem14  27585  mulsass  27621  precsexlemcbv  27652  axlowdimlem3  28202  axlowdimlem17  28216  ex-un  29677  ex-pw  29682  indifundif  31762  iuninc  31792  difico  31994  esum2dlem  33090  fiunelcarsg  33315  carsgclctunlem1  33316  carsggect  33317  bnj601  33931  bnj1416  34050  subfacp1lem1  34170  cvmliftlem10  34285  satf0  34363  poimirlem4  36492  poimirlem18  36506  poimirlem21  36509  poimirlem22  36510  poimirlem25  36513  mbfresfi  36534  asindmre  36571  fsuppssind  41165  mapfzcons  41454  mapfzcons1  41455  diophin  41510  iocunico  41960  rp-fakeuninass  42267  rclexi  42366  rtrclex  42368  dfrtrcl5  42380  dfrcl2  42425  corcltrcl  42490  cotrclrcl  42493  frege109d  42508  frege131d  42515  fiiuncl  43752  cnrefiisp  44546  fourierdlem65  44887  fourierdlem89  44911  fourierdlem90  44912  fourierdlem91  44913  fourierdlem96  44918  fourierdlem97  44919  fourierdlem98  44920  fourierdlem99  44921  fourierdlem100  44922  fourierdlem105  44927  fourierdlem108  44930  fourierdlem109  44931  fourierdlem110  44932  fourierdlem112  44934  fourierdlem113  44935  isomenndlem  45246  hoidmvlelem3  45313  1fzopredsuc  46032  lmod1zr  47174