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

Theorem uneq2i 3907
 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 3904 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1632   ∪ cun 3713 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-un 3720 This theorem is referenced by:  un4  3916  unundir  3918  difdif2  4027  difun2  4192  difdifdir  4200  dfif5  4246  qdass  4432  qdassr  4433  ssunpr  4510  iununi  4762  unidif0  4987  difxp1  5717  unisuc  5962  iunsuc  5968  fresaun  6236  fresaunres2  6237  fvssunirn  6379  fmptap  6601  fvsnun1  6613  funiunfv  6670  onuninsuci  7206  wfrlem13  7597  wfrlem14  7598  wfrlem16  7600  tfrlem10  7653  oarec  7813  dfdom2  8149  fodomr  8278  ranksuc  8903  kmlem3  9186  fin1a2lem10  9443  fin1a2lem12  9445  axdc3lem4  9487  prunioo  12514  fz0sn0fz1  12670  facnn  13276  fac0  13277  hashun3  13385  trclublem  13955  dmtrclfv  13978  fsum2dlem  14720  fsumiun  14772  incexclem  14787  fprod2dlem  14929  prmreclem4  15845  strlemor1OLD  16191  strlemor2OLD  16192  strlemor3OLD  16193  phlstr  16256  mreexexlem4d  16529  opsrtoslem2  19707  restcld  21198  neitr  21206  fiuncmp  21429  refun0  21540  1stckgenlem  21578  filconn  21908  ufildr  21956  alexsubALTlem3  22074  ptcmplem1  22077  restmetu  22596  ovolfiniun  23489  unmbl  23525  volfiniun  23535  voliunlem1  23538  plyun0  24172  lgsquadlem3  25327  axlowdimlem3  26044  axlowdimlem17  26058  ex-un  27613  ex-pw  27618  indifundif  29684  iuninc  29707  difico  29875  esum2dlem  30484  fiunelcarsg  30708  carsgclctunlem1  30709  carsggect  30710  bnj601  31318  bnj1416  31435  subfacp1lem1  31489  cvmliftlem10  31604  noextend  32146  noextendseq  32147  nosupbday  32178  nosupbnd1  32187  nosupbnd2  32189  noetalem2  32191  noetalem3  32192  noetalem4  32193  poimirlem4  33744  poimirlem18  33758  poimirlem21  33761  poimirlem22  33762  poimirlem25  33765  mbfresfi  33787  asindmre  33826  mapfzcons  37799  mapfzcons1  37800  diophin  37856  iocunico  38316  rp-fakeuninass  38382  rclexi  38442  rtrclex  38444  dfrtrcl5  38456  dfrcl2  38486  corcltrcl  38551  cotrclrcl  38554  frege109d  38569  frege131d  38576  fiiuncl  39751  cnrefiisp  40577  fourierdlem65  40909  fourierdlem89  40933  fourierdlem90  40934  fourierdlem91  40935  fourierdlem96  40940  fourierdlem97  40941  fourierdlem98  40942  fourierdlem99  40943  fourierdlem100  40944  fourierdlem105  40949  fourierdlem108  40952  fourierdlem109  40953  fourierdlem110  40954  fourierdlem112  40956  fourierdlem113  40957  isomenndlem  41268  hoidmvlelem3  41335  1fzopredsuc  41862  lmod1zr  42810
 Copyright terms: Public domain W3C validator