Theorem uneq2i 4066

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

Syntax hints:   = wceq 1539   ∪ cun 3857

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-un 3864

This theorem is referenced by:  un4  4075  unundir  4077  difdif2  4192  difun2  4378  difdifdir  4386  dfif5  4437  qdass  4647  qdassr  4648  ssunpr  4723  iununi  4987  unidif0  5229  difxp1  5995  unisuc  6246  iunsuc  6252  fresaun  6535  fresaunres2  6536  fvssunirn  6688  fmptap  6924  fvsnun1  6936  funiunfv  7000  onuninsuci  7555  wfrlem13  7978  wfrlem14  7979  wfrlem16  7981  tfrlem10  8034  oarec  8199  dfdom2  8554  fodomr  8690  ranksuc  9320  kmlem3  9605  djuassen  9631  fin1a2lem10  9862  fin1a2lem12  9864  axdc3lem4  9906  prunioo  12906  fz0sn0fz1  13066  facnn  13678  fac0  13679  hashun3  13788  trclublem  14395  dmtrclfv  14418  fsum2dlem  15166  fsumiun  15217  incexclem  15232  fprod2dlem  15375  prmreclem4  16303  phlstr  16704  mreexexlem4d  16969  smndex1basss  18129  smndex1mgm  18131  opsrtoslem2  20809  restcld  21865  neitr  21873  fiuncmp  22097  refun0  22208  1stckgenlem  22246  filconn  22576  ufildr  22624  alexsubALTlem3  22742  ptcmplem1  22745  restmetu  23265  ovolfiniun  24194  unmbl  24230  volfiniun  24240  voliunlem1  24243  plyun0  24886  lgsquadlem3  26058  axlowdimlem3  26830  axlowdimlem17  26844  ex-un  28301  ex-pw  28306  indifundif  30388  iuninc  30415  difico  30621  esum2dlem  31572  fiunelcarsg  31795  carsgclctunlem1  31796  carsggect  31797  bnj601  32413  bnj1416  32532  subfacp1lem1  32650  cvmliftlem10  32765  satf0  32843  frrlem14  33390  noextend  33427  noextendseq  33428  nosupbday  33466  nosupbnd1  33475  nosupbnd2  33477  noinfbday  33481  noinfbnd1  33490  noinfbnd2  33492  noetasuplem2  33495  noetasuplem3  33496  noetasuplem4  33497  noetainflem4  33501  poimirlem4  35334  poimirlem18  35348  poimirlem21  35351  poimirlem22  35352  poimirlem25  35355  mbfresfi  35376  asindmre  35413  fsuppssind  39780  mapfzcons  40023  mapfzcons1  40024  diophin  40079  iocunico  40527  rp-fakeuninass  40590  rclexi  40681  rtrclex  40683  dfrtrcl5  40695  dfrcl2  40741  corcltrcl  40806  cotrclrcl  40809  frege109d  40824  frege131d  40831  fiiuncl  42065  cnrefiisp  42831  fourierdlem65  43172  fourierdlem89  43196  fourierdlem90  43197  fourierdlem91  43198  fourierdlem96  43203  fourierdlem97  43204  fourierdlem98  43205  fourierdlem99  43206  fourierdlem100  43207  fourierdlem105  43212  fourierdlem108  43215  fourierdlem109  43216  fourierdlem110  43217  fourierdlem112  43219  fourierdlem113  43220  isomenndlem  43528  hoidmvlelem3  43595  1fzopredsuc  44242  lmod1zr  45260