Theorem uneq2i 4138

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

Syntax hints:   = wceq 1537   ∪ cun 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943

This theorem is referenced by:  un4  4147  unundir  4149  difdif2  4263  difun2  4431  difdifdir  4439  dfif5  4485  qdass  4691  qdassr  4692  ssunpr  4767  iununi  5023  unidif0  5262  difxp1  6024  unisuc  6269  iunsuc  6275  fresaun  6551  fresaunres2  6552  fvssunirn  6701  fmptap  6934  fvsnun1  6946  funiunfv  7009  onuninsuci  7557  wfrlem13  7969  wfrlem14  7970  wfrlem16  7972  tfrlem10  8025  oarec  8190  dfdom2  8537  fodomr  8670  ranksuc  9296  kmlem3  9580  djuassen  9606  fin1a2lem10  9833  fin1a2lem12  9835  axdc3lem4  9877  prunioo  12870  fz0sn0fz1  13027  facnn  13638  fac0  13639  hashun3  13748  trclublem  14357  dmtrclfv  14380  fsum2dlem  15127  fsumiun  15178  incexclem  15193  fprod2dlem  15336  prmreclem4  16257  phlstr  16655  mreexexlem4d  16920  smndex1basss  18072  smndex1mgm  18074  opsrtoslem2  20267  restcld  21782  neitr  21790  fiuncmp  22014  refun0  22125  1stckgenlem  22163  filconn  22493  ufildr  22541  alexsubALTlem3  22659  ptcmplem1  22662  restmetu  23182  ovolfiniun  24104  unmbl  24140  volfiniun  24150  voliunlem1  24153  plyun0  24789  lgsquadlem3  25960  axlowdimlem3  26732  axlowdimlem17  26746  ex-un  28205  ex-pw  28210  indifundif  30287  iuninc  30314  difico  30508  esum2dlem  31353  fiunelcarsg  31576  carsgclctunlem1  31577  carsggect  31578  bnj601  32194  bnj1416  32313  subfacp1lem1  32428  cvmliftlem10  32543  satf0  32621  frrlem14  33138  noextend  33175  noextendseq  33176  nosupbday  33207  nosupbnd1  33216  nosupbnd2  33218  noetalem2  33220  noetalem3  33221  noetalem4  33222  poimirlem4  34898  poimirlem18  34912  poimirlem21  34915  poimirlem22  34916  poimirlem25  34919  mbfresfi  34940  asindmre  34979  mapfzcons  39320  mapfzcons1  39321  diophin  39376  iocunico  39824  rp-fakeuninass  39889  rclexi  39982  rtrclex  39984  dfrtrcl5  39996  dfrcl2  40026  corcltrcl  40091  cotrclrcl  40094  frege109d  40109  frege131d  40116  fiiuncl  41334  cnrefiisp  42118  fourierdlem65  42463  fourierdlem89  42487  fourierdlem90  42488  fourierdlem91  42489  fourierdlem96  42494  fourierdlem97  42495  fourierdlem98  42496  fourierdlem99  42497  fourierdlem100  42498  fourierdlem105  42503  fourierdlem108  42506  fourierdlem109  42507  fourierdlem110  42508  fourierdlem112  42510  fourierdlem113  42511  isomenndlem  42819  hoidmvlelem3  42886  1fzopredsuc  43531  lmod1zr  44555