Theorem uneq2i 4127

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

Syntax hints:   = wceq 1567   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918

This theorem is referenced by:  un4  4136  unundir  4138  difdif2  4257  difun2  4447  difdifdir  4457  dfif5  4509  qdass  4724  qdassr  4725  ssunpr  4803  iununi  5069  unidif0  5331  unidif0OLD  5332  difxp1  6163  iunsuc  6449  fresaun  6750  fresaunres2  6751  fmptap  7169  fvsnun1  7181  funiunfv  7247  onuninsuci  7835  frrlem14  8295  tfrlem10  8373  oarec  8546  dfdom2  8974  fodomr  9115  fodomfir  9286  ranksuc  9836  kmlem3  10135  djuassen  10161  fin1a2lem10  10392  fin1a2lem12  10394  axdc3lem4  10436  prunioo  13507  fz0sn0fz1  13672  facnn  14310  fac0  14311  hashun3  14419  trclublem  15031  dmtrclfv  15054  fsum2dlem  15820  fsumiun  15872  incexclem  15889  fprod2dlem  16033  prmreclem4  16978  phlstr  17398  mreexexlem4d  17702  smndex1basss  18966  smndex1mgm  18968  opsrtoslem2  22175  restcld  23297  neitr  23305  fiuncmp  23529  refun0  23640  1stckgenlem  23678  filconn  24008  ufildr  24056  alexsubALTlem3  24174  ptcmplem1  24177  restmetu  24695  ovolfiniun  25628  unmbl  25664  volfiniun  25674  voliunlem1  25677  plyun0  26322  lgsquadlem3  27511  noextend  27795  noextendseq  27796  nosupbday  27834  nosupbnd1  27843  nosupbnd2  27845  noinfbday  27849  noinfbnd1  27858  noinfbnd2  27860  noetasuplem2  27863  noetasuplem3  27864  noetasuplem4  27865  noetainflem4  27869  madeun  28042  addsproplem2  28128  addsasslem1  28161  addsasslem2  28162  negsproplem2  28187  negsproplem6  28191  negsid  28199  mulsproplem2  28275  mulsproplem3  28276  mulsproplem4  28277  mulsproplem12  28285  mulsproplem13  28286  mulsproplem14  28287  mulsass  28324  precsexlemcbv  28364  onmulscl  28436  axlowdimlem3  29234  axlowdimlem17  29248  ex-un  30715  ex-pw  30720  indifundif  32810  iuninc  32845  difico  33068  esum2dlem  34426  fiunelcarsg  34650  carsgclctunlem1  34651  carsggect  34652  bnj601  35252  bnj1416  35371  subfacp1lem1  35569  cvmliftlem10  35684  satf0  35762  poimirlem4  38162  poimirlem18  38176  poimirlem21  38179  poimirlem22  38180  poimirlem25  38183  mbfresfi  38204  asindmre  38241  dmuncnvepres  38929  blockadjliftmap  38996  fsuppssind  43216  mapfzcons  43338  mapfzcons1  43339  diophin  43394  iocunico  43829  rp-fakeuninass  44133  rclexi  44232  rtrclex  44234  dfrtrcl5  44246  dfrcl2  44291  corcltrcl  44356  cotrclrcl  44359  frege109d  44374  frege131d  44381  nregmodelf1o  45615  fiiuncl  45676  cnrefiisp  46435  fourierdlem65  46776  fourierdlem89  46800  fourierdlem90  46801  fourierdlem91  46802  fourierdlem96  46807  fourierdlem97  46808  fourierdlem98  46809  fourierdlem99  46810  fourierdlem100  46811  fourierdlem105  46816  fourierdlem108  46819  fourierdlem109  46820  fourierdlem110  46821  fourierdlem112  46823  fourierdlem113  46824  isomenndlem  47135  hoidmvlelem3  47202  1fzopredsuc  47950  dfclnbgr4  48477  clnbupgr  48486  usgrexmpl2edg  48682  lmod1zr  49157  dftpos5  49536  dftpos6  49537  tposresg  49540  tposrescnv  49541  tposres3  49543