Theorem uneq2i 3764

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

Syntax hints:   = wceq 1483   ∪ cun 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579

This theorem is referenced by:  un4  3773  unundir  3775  difdif2  3884  difun2  4048  difdifdir  4056  dfif5  4102  qdass  4288  qdassr  4289  ssunpr  4365  iununi  4610  unidif0  4838  difxp1  5559  unisuc  5801  iunsuc  5807  fresaun  6075  fresaunres2  6076  fvssunirn  6217  fmptap  6436  fvsnun1  6448  funiunfv  6506  onuninsuci  7040  wfrlem13  7427  wfrlem14  7428  wfrlem16  7430  tfrlem10  7483  oarec  7642  dfdom2  7981  fodomr  8111  ranksuc  8728  kmlem3  8974  fin1a2lem10  9231  fin1a2lem12  9233  axdc3lem4  9275  prunioo  12301  fz0sn0fz1  12456  facnn  13062  fac0  13063  hashun3  13173  trclublem  13734  dmtrclfv  13759  fsum2dlem  14501  fsumiun  14553  incexclem  14568  fprod2dlem  14710  prmreclem4  15623  strlemor1OLD  15969  strlemor2OLD  15970  strlemor3OLD  15971  phlstr  16034  mreexexlem4d  16307  opsrtoslem2  19485  restcld  20976  neitr  20984  fiuncmp  21207  refun0  21318  1stckgenlem  21356  filconn  21687  ufildr  21735  alexsubALTlem3  21853  ptcmplem1  21856  restmetu  22375  ovolfiniun  23269  unmbl  23305  volfiniun  23315  voliunlem1  23318  plyun0  23953  lgsquadlem3  25107  axlowdimlem3  25824  axlowdimlem17  25838  ex-un  27281  ex-pw  27286  indifundif  29356  iuninc  29379  difico  29545  esum2dlem  30154  fiunelcarsg  30378  carsgclctunlem1  30379  carsggect  30380  bnj601  30990  bnj1416  31107  subfacp1lem1  31161  cvmliftlem10  31276  noextend  31819  noextendseq  31820  nosupbday  31851  nosupbnd1  31860  nosupbnd2  31862  noetalem2  31864  noetalem3  31865  noetalem4  31866  poimirlem4  33413  poimirlem18  33427  poimirlem21  33430  poimirlem22  33431  poimirlem25  33434  mbfresfi  33456  asindmre  33495  mapfzcons  37279  mapfzcons1  37280  diophin  37336  iocunico  37796  rp-fakeuninass  37862  rclexi  37922  rtrclex  37924  dfrtrcl5  37936  dfrcl2  37966  corcltrcl  38031  cotrclrcl  38034  frege109d  38049  frege131d  38056  fiiuncl  39234  cnrefiisp  40056  fourierdlem65  40388  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem96  40419  fourierdlem97  40420  fourierdlem98  40421  fourierdlem99  40422  fourierdlem100  40423  fourierdlem105  40428  fourierdlem108  40431  fourierdlem109  40432  fourierdlem110  40433  fourierdlem112  40435  fourierdlem113  40436  isomenndlem  40744  hoidmvlelem3  40811  1fzopredsuc  41334  lmod1zr  42282