Theorem uneq2i 4167

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

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 4152

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154

This theorem is used by:  un4  4176  unundir  4178  difdif2  4244  difun2  4440  difdifdir  4450  dfif5  4502  qdass  4716  qdassr  4717  ssunpr  4794  iununi  5064  unidif0  5328  unidif0OLD  5329  difxp1  6174  iunsuc  6476  fresaun  6783  fresaunres2  6784  fmptap  7206  fvsnun1  7218  funiunfv  7283  onuninsuci  7885  frrlem14  8355  tfrlem10  8433  oarec  8608  dfdom2  9043  fodomr  9185  fodomfir  9357  ranksuc  9919  kmlem3  10270  djuassen  10296  fin1a2lem10  10526  fin1a2lem12  10528  axdc3lem4  10570  prunioo  13652  fz0sn0fz1  13819  facnn  14460  fac0  14461  hashun3  14569  trclublem  15191  dmtrclfv  15214  fsum2dlem  15980  fsumiun  16032  incexclem  16049  fprod2dlem  16191  prmreclem4  17141  phlstr  17563  mreexexlem4d  17871  smndex1basss  19154  smndex1mgm  19156  opsrtoslem2  22420  restcld  23545  neitr  23553  fiuncmp  23777  refun0  23889  1stckgenlem  23927  filconn  24257  ufildr  24305  alexsubALTlem3  24423  ptcmplem1  24426  restmetu  24944  ovolfiniun  25877  unmbl  25913  volfiniun  25923  voliunlem1  25926  plyun0  26570  lgsquadlem3  27766  noextend  28080  noextendseq  28081  nosupbday  28119  nosupbnd1  28128  nosupbnd2  28130  noinfbday  28134  noinfbnd1  28143  noinfbnd2  28145  noetasuplem2  28148  noetasuplem3  28149  noetasuplem4  28150  noetainflem4  28154  madeun  28327  addsproplem2  28413  addsasslem1  28446  addsasslem2  28447  negsproplem2  28472  negsproplem6  28476  negsid  28484  mulsproplem2  28560  mulsproplem3  28561  mulsproplem4  28562  mulsproplem12  28570  mulsproplem13  28571  mulsproplem14  28572  mulsass  28609  precsexlemcbv  28649  onmulscl  28721  axlowdimlem3  29579  axlowdimlem17  29593  ex-un  31082  ex-pw  31087  indifundif  33219  iuninc  33253  difico  33471  esum2dlem  34835  fiunelcarsg  35059  carsgclctunlem1  35060  carsggect  35061  bnj601  35661  bnj1416  35780  subfacp1lem1  36152  cvmliftlem10  36267  satf0  36345  poimirlem4  38810  poimirlem18  38824  poimirlem21  38827  poimirlem22  38828  poimirlem25  38831  mbfresfi  38852  asindmre  38889  dmuncnvepres  39589  blockadjliftmap  39656  fsuppssind  43887  mapfzcons  43993  mapfzcons1  43994  diophin  44049  iocunico  44474  rp-fakeuninass  44778  rclexi  44876  rtrclex  44878  dfrtrcl5  44890  dfrcl2  44935  corcltrcl  45000  cotrclrcl  45003  frege109d  45018  frege131d  45025  nregmodelf1o  46269  fiiuncl  46356  cnrefiisp  47113  fourierdlem65  47454  fourierdlem89  47478  fourierdlem90  47479  fourierdlem91  47480  fourierdlem96  47485  fourierdlem97  47486  fourierdlem98  47487  fourierdlem99  47488  fourierdlem100  47489  fourierdlem105  47494  fourierdlem108  47497  fourierdlem109  47498  fourierdlem110  47499  fourierdlem112  47501  fourierdlem113  47502  isomenndlem  47813  hoidmvlelem3  47880  1fzopredsuc  48668  dfclnbgr4  49195  clnbupgr  49204  usgrexmpl2edg  49400  lmod1zr  49936  dftpos5  50318  dftpos6  50319  tposresg  50322  tposrescnv  50323  tposres3  50325