Theorem uneq2i 4098

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

Syntax hints:   = wceq 1541   ∪ cun 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-un 3896

This theorem is referenced by:  un4  4107  unundir  4109  difdif2  4225  difun2  4419  difdifdir  4427  dfif5  4480  qdass  4694  qdassr  4695  ssunpr  4770  iununi  5032  unidif0  5285  difxp1  6065  unisuc  6339  iunsuc  6345  fresaun  6641  fresaunres2  6642  fvssunirn  6797  fmptap  7036  fvsnun1  7048  funiunfv  7115  onuninsuci  7675  frrlem14  8099  wfrlem13OLD  8136  wfrlem14OLD  8137  wfrlem16OLD  8139  tfrlem10  8202  oarec  8369  dfdom2  8737  fodomr  8880  ranksuc  9607  kmlem3  9892  djuassen  9918  fin1a2lem10  10149  fin1a2lem12  10151  axdc3lem4  10193  prunioo  13195  fz0sn0fz1  13355  facnn  13970  fac0  13971  hashun3  14080  trclublem  14687  dmtrclfv  14710  fsum2dlem  15463  fsumiun  15514  incexclem  15529  fprod2dlem  15671  prmreclem4  16601  phlstr  17037  mreexexlem4d  17337  smndex1basss  18525  smndex1mgm  18527  opsrtoslem2  21244  restcld  22304  neitr  22312  fiuncmp  22536  refun0  22647  1stckgenlem  22685  filconn  23015  ufildr  23063  alexsubALTlem3  23181  ptcmplem1  23184  restmetu  23707  ovolfiniun  24646  unmbl  24682  volfiniun  24692  voliunlem1  24695  plyun0  25339  lgsquadlem3  26511  axlowdimlem3  27293  axlowdimlem17  27307  ex-un  28767  ex-pw  28772  indifundif  30852  iuninc  30879  difico  31083  esum2dlem  32039  fiunelcarsg  32262  carsgclctunlem1  32263  carsggect  32264  bnj601  32879  bnj1416  32998  subfacp1lem1  33120  cvmliftlem10  33235  satf0  33313  noextend  33848  noextendseq  33849  nosupbday  33887  nosupbnd1  33896  nosupbnd2  33898  noinfbday  33902  noinfbnd1  33911  noinfbnd2  33913  noetasuplem2  33916  noetasuplem3  33917  noetasuplem4  33918  noetainflem4  33922  madeun  34045  poimirlem4  35760  poimirlem18  35774  poimirlem21  35777  poimirlem22  35778  poimirlem25  35781  mbfresfi  35802  asindmre  35839  fsuppssind  40262  mapfzcons  40518  mapfzcons1  40519  diophin  40574  iocunico  41022  rp-fakeuninass  41085  rclexi  41176  rtrclex  41178  dfrtrcl5  41190  dfrcl2  41235  corcltrcl  41300  cotrclrcl  41303  frege109d  41318  frege131d  41325  fiiuncl  42566  cnrefiisp  43325  fourierdlem65  43666  fourierdlem89  43690  fourierdlem90  43691  fourierdlem91  43692  fourierdlem96  43697  fourierdlem97  43698  fourierdlem98  43699  fourierdlem99  43700  fourierdlem100  43701  fourierdlem105  43706  fourierdlem108  43709  fourierdlem109  43710  fourierdlem110  43711  fourierdlem112  43713  fourierdlem113  43714  isomenndlem  44022  hoidmvlelem3  44089  1fzopredsuc  44768  lmod1zr  45786