Theorem uneq2i 4160

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

Syntax hints:   = wceq 1540   ∪ cun 3946

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3953

This theorem is referenced by:  un4  4169  unundir  4171  difdif2  4286  difun2  4480  difdifdir  4491  dfif5  4544  qdass  4757  qdassr  4758  ssunpr  4835  iununi  5102  unidif0  5358  difxp1  6164  iunsuc  6449  fresaun  6762  fresaunres2  6763  fvssunirnOLD  6925  fmptap  7170  fvsnun1  7182  funiunfv  7250  onuninsuci  7833  frrlem14  8290  wfrlem13OLD  8327  wfrlem14OLD  8328  wfrlem16OLD  8330  tfrlem10  8393  oarec  8568  dfdom2  8980  fodomr  9134  ranksuc  9866  kmlem3  10153  djuassen  10179  fin1a2lem10  10410  fin1a2lem12  10412  axdc3lem4  10454  prunioo  13465  fz0sn0fz1  13625  facnn  14242  fac0  14243  hashun3  14351  trclublem  14949  dmtrclfv  14972  fsum2dlem  15723  fsumiun  15774  incexclem  15789  fprod2dlem  15931  prmreclem4  16859  phlstr  17298  mreexexlem4d  17598  smndex1basss  18825  smndex1mgm  18827  opsrtoslem2  21841  restcld  22909  neitr  22917  fiuncmp  23141  refun0  23252  1stckgenlem  23290  filconn  23620  ufildr  23668  alexsubALTlem3  23786  ptcmplem1  23789  restmetu  24312  ovolfiniun  25263  unmbl  25299  volfiniun  25309  voliunlem1  25312  plyun0  25960  lgsquadlem3  27136  noextend  27420  noextendseq  27421  nosupbday  27459  nosupbnd1  27468  nosupbnd2  27470  noinfbday  27474  noinfbnd1  27483  noinfbnd2  27485  noetasuplem2  27488  noetasuplem3  27489  noetasuplem4  27490  noetainflem4  27494  madeun  27630  addsproplem2  27707  addsasslem1  27740  addsasslem2  27741  negsproplem2  27757  negsproplem6  27761  negsid  27769  mulsproplem2  27827  mulsproplem3  27828  mulsproplem4  27829  mulsproplem12  27837  mulsproplem13  27838  mulsproplem14  27839  mulsass  27875  precsexlemcbv  27906  axlowdimlem3  28484  axlowdimlem17  28498  ex-un  29959  ex-pw  29964  indifundif  32044  iuninc  32074  difico  32276  esum2dlem  33403  fiunelcarsg  33628  carsgclctunlem1  33629  carsggect  33630  bnj601  34244  bnj1416  34363  subfacp1lem1  34483  cvmliftlem10  34598  satf0  34676  poimirlem4  36808  poimirlem18  36822  poimirlem21  36825  poimirlem22  36826  poimirlem25  36829  mbfresfi  36850  asindmre  36887  fsuppssind  41480  mapfzcons  41769  mapfzcons1  41770  diophin  41825  iocunico  42275  rp-fakeuninass  42582  rclexi  42681  rtrclex  42683  dfrtrcl5  42695  dfrcl2  42740  corcltrcl  42805  cotrclrcl  42808  frege109d  42823  frege131d  42830  fiiuncl  44066  cnrefiisp  44857  fourierdlem65  45198  fourierdlem89  45222  fourierdlem90  45223  fourierdlem91  45224  fourierdlem96  45229  fourierdlem97  45230  fourierdlem98  45231  fourierdlem99  45232  fourierdlem100  45233  fourierdlem105  45238  fourierdlem108  45241  fourierdlem109  45242  fourierdlem110  45243  fourierdlem112  45245  fourierdlem113  45246  isomenndlem  45557  hoidmvlelem3  45624  1fzopredsuc  46343  lmod1zr  47274