Theorem uneq2i 3991

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

Syntax hints:   = wceq 1656   ∪ cun 3796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-un 3803

This theorem is referenced by:  un4  4000  unundir  4002  difdif2  4114  difun2  4271  difdifdir  4279  dfif5  4322  qdass  4506  qdassr  4507  ssunpr  4581  iununi  4831  unidif0  5060  difxp1  5800  unisuc  6039  iunsuc  6045  fresaun  6312  fresaunres2  6313  fvssunirn  6462  fmptap  6688  fvsnun1  6702  fvsnun1OLD  6704  funiunfv  6761  onuninsuci  7301  wfrlem13  7693  wfrlem14  7694  wfrlem16  7696  tfrlem10  7749  oarec  7909  dfdom2  8248  fodomr  8380  ranksuc  9005  kmlem3  9289  fin1a2lem10  9546  fin1a2lem12  9548  axdc3lem4  9590  prunioo  12594  fz0sn0fz1  12751  facnn  13355  fac0  13356  hashun3  13463  trclublem  14113  dmtrclfv  14136  fsum2dlem  14876  fsumiun  14927  incexclem  14942  fprod2dlem  15083  prmreclem4  15994  phlstr  16393  mreexexlem4d  16660  opsrtoslem2  19845  restcld  21347  neitr  21355  fiuncmp  21578  refun0  21689  1stckgenlem  21727  filconn  22057  ufildr  22105  alexsubALTlem3  22223  ptcmplem1  22226  restmetu  22745  ovolfiniun  23667  unmbl  23703  volfiniun  23713  voliunlem1  23716  plyun0  24352  lgsquadlem3  25520  axlowdimlem3  26243  axlowdimlem17  26257  ex-un  27828  ex-pw  27833  indifundif  29893  iuninc  29915  difico  30081  esum2dlem  30688  fiunelcarsg  30912  carsgclctunlem1  30913  carsggect  30914  bnj601  31525  bnj1416  31642  subfacp1lem1  31696  cvmliftlem10  31811  noextend  32347  noextendseq  32348  nosupbday  32379  nosupbnd1  32388  nosupbnd2  32390  noetalem2  32392  noetalem3  32393  noetalem4  32394  poimirlem4  33950  poimirlem18  33964  poimirlem21  33967  poimirlem22  33968  poimirlem25  33971  mbfresfi  33992  asindmre  34031  mapfzcons  38116  mapfzcons1  38117  diophin  38173  iocunico  38631  rp-fakeuninass  38696  rclexi  38756  rtrclex  38758  dfrtrcl5  38770  dfrcl2  38800  corcltrcl  38865  cotrclrcl  38868  frege109d  38883  frege131d  38890  fiiuncl  40044  cnrefiisp  40844  fourierdlem65  41175  fourierdlem89  41199  fourierdlem90  41200  fourierdlem91  41201  fourierdlem96  41206  fourierdlem97  41207  fourierdlem98  41208  fourierdlem99  41209  fourierdlem100  41210  fourierdlem105  41215  fourierdlem108  41218  fourierdlem109  41219  fourierdlem110  41220  fourierdlem112  41222  fourierdlem113  41223  isomenndlem  41531  hoidmvlelem3  41598  1fzopredsuc  42215  lmod1zr  43122