Theorem uneq2i 4175

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

Syntax hints:   = wceq 1537   ∪ cun 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968

This theorem is referenced by:  un4  4185  unundir  4187  difdif2  4302  difun2  4487  difdifdir  4498  dfif5  4547  qdass  4758  qdassr  4759  ssunpr  4839  iununi  5104  unidif0  5366  difxp1  6187  iunsuc  6471  fresaun  6780  fresaunres2  6781  fvssunirnOLD  6941  fmptap  7190  fvsnun1  7202  funiunfv  7268  onuninsuci  7861  frrlem14  8323  wfrlem13OLD  8360  wfrlem14OLD  8361  wfrlem16OLD  8363  tfrlem10  8426  oarec  8599  dfdom2  9017  fodomr  9167  fodomfir  9366  ranksuc  9903  kmlem3  10191  djuassen  10217  fin1a2lem10  10447  fin1a2lem12  10449  axdc3lem4  10491  prunioo  13518  fz0sn0fz1  13682  facnn  14311  fac0  14312  hashun3  14420  trclublem  15031  dmtrclfv  15054  fsum2dlem  15803  fsumiun  15854  incexclem  15869  fprod2dlem  16013  prmreclem4  16953  phlstr  17392  mreexexlem4d  17692  smndex1basss  18931  smndex1mgm  18933  opsrtoslem2  22098  restcld  23196  neitr  23204  fiuncmp  23428  refun0  23539  1stckgenlem  23577  filconn  23907  ufildr  23955  alexsubALTlem3  24073  ptcmplem1  24076  restmetu  24599  ovolfiniun  25550  unmbl  25586  volfiniun  25596  voliunlem1  25599  plyun0  26251  lgsquadlem3  27441  noextend  27726  noextendseq  27727  nosupbday  27765  nosupbnd1  27774  nosupbnd2  27776  noinfbday  27780  noinfbnd1  27789  noinfbnd2  27791  noetasuplem2  27794  noetasuplem3  27795  noetasuplem4  27796  noetainflem4  27800  madeun  27937  addsproplem2  28018  addsasslem1  28051  addsasslem2  28052  negsproplem2  28076  negsproplem6  28080  negsid  28088  mulsproplem2  28158  mulsproplem3  28159  mulsproplem4  28160  mulsproplem12  28168  mulsproplem13  28169  mulsproplem14  28170  mulsass  28207  precsexlemcbv  28245  onmulscl  28302  axlowdimlem3  28974  axlowdimlem17  28988  ex-un  30453  ex-pw  30458  indifundif  32552  iuninc  32581  difico  32792  esum2dlem  34073  fiunelcarsg  34298  carsgclctunlem1  34299  carsggect  34300  bnj601  34913  bnj1416  35032  subfacp1lem1  35164  cvmliftlem10  35279  satf0  35357  poimirlem4  37611  poimirlem18  37625  poimirlem21  37628  poimirlem22  37629  poimirlem25  37632  mbfresfi  37653  asindmre  37690  fsuppssind  42580  mapfzcons  42704  mapfzcons1  42705  diophin  42760  iocunico  43200  rp-fakeuninass  43506  rclexi  43605  rtrclex  43607  dfrtrcl5  43619  dfrcl2  43664  corcltrcl  43729  cotrclrcl  43732  frege109d  43747  frege131d  43754  fiiuncl  45005  cnrefiisp  45786  fourierdlem65  46127  fourierdlem89  46151  fourierdlem90  46152  fourierdlem91  46153  fourierdlem96  46158  fourierdlem97  46159  fourierdlem98  46160  fourierdlem99  46161  fourierdlem100  46162  fourierdlem105  46167  fourierdlem108  46170  fourierdlem109  46171  fourierdlem110  46172  fourierdlem112  46174  fourierdlem113  46175  isomenndlem  46486  hoidmvlelem3  46553  1fzopredsuc  47274  dfclnbgr4  47749  clnbupgr  47758  usgrexmpl2edg  47924  lmod1zr  48339