Theorem uneq2i 4135

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

Syntax hints:   = wceq 1533   ∪ cun 3933

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 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3940

This theorem is referenced by:  un4  4144  unundir  4146  difdif2  4260  difun2  4428  difdifdir  4436  dfif5  4482  qdass  4682  qdassr  4683  ssunpr  4758  iununi  5013  unidif0  5252  difxp1  6016  unisuc  6261  iunsuc  6267  fresaun  6543  fresaunres2  6544  fvssunirn  6693  fmptap  6926  fvsnun1  6938  funiunfv  7001  onuninsuci  7549  wfrlem13  7961  wfrlem14  7962  wfrlem16  7964  tfrlem10  8017  oarec  8182  dfdom2  8529  fodomr  8662  ranksuc  9288  kmlem3  9572  djuassen  9598  fin1a2lem10  9825  fin1a2lem12  9827  axdc3lem4  9869  prunioo  12861  fz0sn0fz1  13018  facnn  13629  fac0  13630  hashun3  13739  trclublem  14349  dmtrclfv  14372  fsum2dlem  15119  fsumiun  15170  incexclem  15185  fprod2dlem  15328  prmreclem4  16249  phlstr  16647  mreexexlem4d  16912  smndex1basss  18064  smndex1mgm  18066  opsrtoslem2  20259  restcld  21774  neitr  21782  fiuncmp  22006  refun0  22117  1stckgenlem  22155  filconn  22485  ufildr  22533  alexsubALTlem3  22651  ptcmplem1  22654  restmetu  23174  ovolfiniun  24096  unmbl  24132  volfiniun  24142  voliunlem1  24145  plyun0  24781  lgsquadlem3  25952  axlowdimlem3  26724  axlowdimlem17  26738  ex-un  28197  ex-pw  28202  indifundif  30279  iuninc  30306  difico  30500  esum2dlem  31346  fiunelcarsg  31569  carsgclctunlem1  31570  carsggect  31571  bnj601  32187  bnj1416  32306  subfacp1lem1  32421  cvmliftlem10  32536  satf0  32614  frrlem14  33131  noextend  33168  noextendseq  33169  nosupbday  33200  nosupbnd1  33209  nosupbnd2  33211  noetalem2  33213  noetalem3  33214  noetalem4  33215  poimirlem4  34890  poimirlem18  34904  poimirlem21  34907  poimirlem22  34908  poimirlem25  34911  mbfresfi  34932  asindmre  34971  mapfzcons  39306  mapfzcons1  39307  diophin  39362  iocunico  39810  rp-fakeuninass  39875  rclexi  39968  rtrclex  39970  dfrtrcl5  39982  dfrcl2  40012  corcltrcl  40077  cotrclrcl  40080  frege109d  40095  frege131d  40102  fiiuncl  41320  cnrefiisp  42104  fourierdlem65  42450  fourierdlem89  42474  fourierdlem90  42475  fourierdlem91  42476  fourierdlem96  42481  fourierdlem97  42482  fourierdlem98  42483  fourierdlem99  42484  fourierdlem100  42485  fourierdlem105  42490  fourierdlem108  42493  fourierdlem109  42494  fourierdlem110  42495  fourierdlem112  42497  fourierdlem113  42498  isomenndlem  42806  hoidmvlelem3  42873  1fzopredsuc  43518  lmod1zr  44542