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

Theorem uneq2i 3756
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 3753 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  cun 3565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-un 3572
This theorem is referenced by:  un4  3765  unundir  3767  difdif2  3876  difun2  4039  difdifdir  4047  dfif5  4093  qdass  4279  qdassr  4280  ssunpr  4356  iununi  4601  unidif0  4829  difxp1  5547  unisuc  5789  iunsuc  5795  fresaun  6062  fresaunres2  6063  fvssunirn  6204  fmptap  6421  fvsnun1  6433  funiunfv  6491  onuninsuci  7025  wfrlem13  7412  wfrlem14  7413  wfrlem16  7415  tfrlem10  7468  oarec  7627  dfdom2  7966  fodomr  8096  ranksuc  8713  kmlem3  8959  fin1a2lem10  9216  fin1a2lem12  9218  axdc3lem4  9260  prunioo  12286  fz0sn0fz1  12440  facnn  13045  fac0  13046  hashun3  13156  trclublem  13715  dmtrclfv  13740  fsum2dlem  14482  fsumiun  14534  incexclem  14549  fprod2dlem  14691  prmreclem4  15604  strlemor1OLD  15950  strlemor2OLD  15951  strlemor3OLD  15952  phlstr  16015  mreexexlem4d  16288  opsrtoslem2  19466  restcld  20957  neitr  20965  fiuncmp  21188  refun0  21299  1stckgenlem  21337  filconn  21668  ufildr  21716  alexsubALTlem3  21834  ptcmplem1  21837  restmetu  22356  ovolfiniun  23250  unmbl  23286  volfiniun  23296  voliunlem1  23299  plyun0  23934  lgsquadlem3  25088  axlowdimlem3  25805  axlowdimlem17  25819  ex-un  27251  ex-pw  27256  indifundif  29328  iuninc  29351  difico  29519  esum2dlem  30128  fiunelcarsg  30352  carsgclctunlem1  30353  carsggect  30354  bnj601  30964  bnj1416  31081  subfacp1lem1  31135  cvmliftlem10  31250  noextend  31793  noextendseq  31794  nosupbday  31825  nosupbnd1  31834  nosupbnd2  31836  noetalem2  31838  noetalem3  31839  noetalem4  31840  poimirlem4  33384  poimirlem18  33398  poimirlem21  33401  poimirlem22  33402  poimirlem25  33405  mbfresfi  33427  asindmre  33466  mapfzcons  37098  mapfzcons1  37099  diophin  37155  iocunico  37615  rp-fakeuninass  37681  rclexi  37741  rtrclex  37743  dfrtrcl5  37755  dfrcl2  37785  corcltrcl  37850  cotrclrcl  37853  frege109d  37868  frege131d  37875  fiiuncl  39054  fourierdlem65  40151  fourierdlem89  40175  fourierdlem90  40176  fourierdlem91  40177  fourierdlem96  40182  fourierdlem97  40183  fourierdlem98  40184  fourierdlem99  40185  fourierdlem100  40186  fourierdlem105  40191  fourierdlem108  40194  fourierdlem109  40195  fourierdlem110  40196  fourierdlem112  40198  fourierdlem113  40199  isomenndlem  40507  hoidmvlelem3  40574  1fzopredsuc  41097  lmod1zr  42047
  Copyright terms: Public domain W3C validator