Theorem uneq2i 4100

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

Syntax hints:   = wceq 1539   ∪ cun 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-un 3897

This theorem is referenced by:  un4  4109  unundir  4111  difdif2  4226  difun2  4420  difdifdir  4428  dfif5  4481  qdass  4693  qdassr  4694  ssunpr  4771  iununi  5035  unidif0  5291  difxp1  6083  iunsuc  6365  fresaun  6675  fresaunres2  6676  fvssunirn  6835  fmptap  7074  fvsnun1  7086  funiunfv  7153  onuninsuci  7719  frrlem14  8146  wfrlem13OLD  8183  wfrlem14OLD  8184  wfrlem16OLD  8186  tfrlem10  8249  oarec  8424  dfdom2  8799  fodomr  8953  ranksuc  9667  kmlem3  9954  djuassen  9980  fin1a2lem10  10211  fin1a2lem12  10213  axdc3lem4  10255  prunioo  13259  fz0sn0fz1  13419  facnn  14035  fac0  14036  hashun3  14144  trclublem  14751  dmtrclfv  14774  fsum2dlem  15527  fsumiun  15578  incexclem  15593  fprod2dlem  15735  prmreclem4  16665  phlstr  17101  mreexexlem4d  17401  smndex1basss  18589  smndex1mgm  18591  opsrtoslem2  21308  restcld  22368  neitr  22376  fiuncmp  22600  refun0  22711  1stckgenlem  22749  filconn  23079  ufildr  23127  alexsubALTlem3  23245  ptcmplem1  23248  restmetu  23771  ovolfiniun  24710  unmbl  24746  volfiniun  24756  voliunlem1  24759  plyun0  25403  lgsquadlem3  26575  axlowdimlem3  27357  axlowdimlem17  27371  ex-un  28833  ex-pw  28838  indifundif  30918  iuninc  30945  difico  31149  esum2dlem  32105  fiunelcarsg  32328  carsgclctunlem1  32329  carsggect  32330  bnj601  32945  bnj1416  33064  subfacp1lem1  33186  cvmliftlem10  33301  satf0  33379  noextend  33914  noextendseq  33915  nosupbday  33953  nosupbnd1  33962  nosupbnd2  33964  noinfbday  33968  noinfbnd1  33977  noinfbnd2  33979  noetasuplem2  33982  noetasuplem3  33983  noetasuplem4  33984  noetainflem4  33988  madeun  34111  poimirlem4  35825  poimirlem18  35839  poimirlem21  35842  poimirlem22  35843  poimirlem25  35846  mbfresfi  35867  asindmre  35904  fsuppssind  40319  mapfzcons  40575  mapfzcons1  40576  diophin  40631  iocunico  41080  rp-fakeuninass  41161  rclexi  41261  rtrclex  41263  dfrtrcl5  41275  dfrcl2  41320  corcltrcl  41385  cotrclrcl  41388  frege109d  41403  frege131d  41410  fiiuncl  42651  cnrefiisp  43420  fourierdlem65  43761  fourierdlem89  43785  fourierdlem90  43786  fourierdlem91  43787  fourierdlem96  43792  fourierdlem97  43793  fourierdlem98  43794  fourierdlem99  43795  fourierdlem100  43796  fourierdlem105  43801  fourierdlem108  43804  fourierdlem109  43805  fourierdlem110  43806  fourierdlem112  43808  fourierdlem113  43809  isomenndlem  44118  hoidmvlelem3  44185  1fzopredsuc  44874  lmod1zr  45892