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

Theorem uneq1i 3741
Description: Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
uneq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
uneq1i (𝐴𝐶) = (𝐵𝐶)

Proof of Theorem uneq1i
StepHypRef Expression
1 uneq1i.1 . 2 𝐴 = 𝐵
2 uneq1 3738 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  cun 3553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-un 3560
This theorem is referenced by:  un12  3749  unundi  3752  undif1  4015  dfif5  4074  tpcoma  4255  qdass  4258  qdassr  4259  tpidm12  4260  symdifv  4564  unidif0  4798  difxp2  5519  resasplit  6031  fresaun  6032  fresaunres2  6033  df2o3  7518  sbthlem6  8019  fodomr  8055  domss2  8063  domunfican  8177  kmlem11  8926  hashfun  13164  prmreclem2  15545  setscom  15824  gsummptfzsplitl  18254  uniioombllem3  23259  lhop  23683  ex-un  27135  ex-pw  27140  indifundif  29203  bnj1415  30814  subfacp1lem1  30869  dftrpred4g  31435  lineunray  31896  bj-2upln1upl  32659  poimirlem3  33044  poimirlem4  33045  poimirlem5  33046  poimirlem16  33057  poimirlem17  33058  poimirlem19  33060  poimirlem20  33061  poimirlem22  33063  dfrcl2  37447  iunrelexp0  37475  trclfvdecomr  37501  corcltrcl  37512  cotrclrcl  37515  df3o2  37804  fourierdlem80  39710  caragenuncllem  40033  carageniuncllem1  40042  1fzopredsuc  40631  nnsum4primeseven  40977  nnsum4primesevenALTV  40978  lmod1  41569
  Copyright terms: Public domain W3C validator