MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uneq2i Structured version   Visualization version   GIF version

Theorem uneq2i 3913
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
StepHypRef Expression
1 uneq1i.1 . 2 𝐴 = 𝐵
2 uneq2 3910 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1630  cun 3719
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-un 3726
This theorem is referenced by:  un4  3922  unundir  3924  difdif2  4031  difun2  4188  difdifdir  4196  dfif5  4239  qdass  4422  qdassr  4423  ssunpr  4496  iununi  4742  unidif0  4966  difxp1  5700  unisuc  5944  iunsuc  5950  fresaun  6215  fresaunres2  6216  fvssunirn  6358  fmptap  6579  fvsnun1  6591  funiunfv  6648  onuninsuci  7186  wfrlem13  7579  wfrlem14  7580  wfrlem16  7582  tfrlem10  7635  oarec  7795  dfdom2  8134  fodomr  8266  ranksuc  8891  kmlem3  9175  fin1a2lem10  9432  fin1a2lem12  9434  axdc3lem4  9476  prunioo  12507  fz0sn0fz1  12663  facnn  13265  fac0  13266  hashun3  13374  trclublem  13943  dmtrclfv  13966  fsum2dlem  14708  fsumiun  14759  incexclem  14774  fprod2dlem  14916  prmreclem4  15829  strlemor1OLD  16176  strlemor2OLD  16177  strlemor3OLD  16178  phlstr  16241  mreexexlem4d  16514  opsrtoslem2  19699  restcld  21196  neitr  21204  fiuncmp  21427  refun0  21538  1stckgenlem  21576  filconn  21906  ufildr  21954  alexsubALTlem3  22072  ptcmplem1  22075  restmetu  22594  ovolfiniun  23488  unmbl  23524  volfiniun  23534  voliunlem1  23537  plyun0  24172  lgsquadlem3  25327  axlowdimlem3  26044  axlowdimlem17  26058  ex-un  27617  ex-pw  27622  indifundif  29688  iuninc  29711  difico  29879  esum2dlem  30488  fiunelcarsg  30712  carsgclctunlem1  30713  carsggect  30714  bnj601  31322  bnj1416  31439  subfacp1lem1  31493  cvmliftlem10  31608  noextend  32150  noextendseq  32151  nosupbday  32182  nosupbnd1  32191  nosupbnd2  32193  noetalem2  32195  noetalem3  32196  noetalem4  32197  poimirlem4  33739  poimirlem18  33753  poimirlem21  33756  poimirlem22  33757  poimirlem25  33760  mbfresfi  33781  asindmre  33820  mapfzcons  37798  mapfzcons1  37799  diophin  37855  iocunico  38315  rp-fakeuninass  38381  rclexi  38441  rtrclex  38443  dfrtrcl5  38455  dfrcl2  38485  corcltrcl  38550  cotrclrcl  38553  frege109d  38568  frege131d  38575  fiiuncl  39749  cnrefiisp  40568  fourierdlem65  40899  fourierdlem89  40923  fourierdlem90  40924  fourierdlem91  40925  fourierdlem96  40930  fourierdlem97  40931  fourierdlem98  40932  fourierdlem99  40933  fourierdlem100  40934  fourierdlem105  40939  fourierdlem108  40942  fourierdlem109  40943  fourierdlem110  40944  fourierdlem112  40946  fourierdlem113  40947  isomenndlem  41258  hoidmvlelem3  41325  1fzopredsuc  41852  lmod1zr  42800
  Copyright terms: Public domain W3C validator