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

Theorem uneq1i 3725
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 3722 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  cun 3538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545
This theorem is referenced by:  un12  3733  unundi  3736  undif1  3995  dfif5  4052  tpcoma  4229  qdass  4232  qdassr  4233  tpidm12  4234  symdifv  4534  unidif0  4764  difxp2  5479  resasplit  5987  fresaun  5988  fresaunres2  5989  df2o3  7460  sbthlem6  7960  fodomr  7996  domss2  8004  domunfican  8118  kmlem11  8865  hashfun  13084  prmreclem2  15459  setscom  15731  gsummptfzsplitl  18156  uniioombllem3  23159  lhop  23583  usgrafilem1  25940  constr3pthlem1  26183  ex-un  26673  ex-pw  26678  indifundif  28740  bnj1415  30360  subfacp1lem1  30415  dftrpred4g  30978  lineunray  31424  bj-2upln1upl  32205  poimirlem3  32582  poimirlem4  32583  poimirlem5  32584  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem22  32601  dfrcl2  36985  iunrelexp0  37013  trclfvdecomr  37039  corcltrcl  37050  cotrclrcl  37053  df3o2  37342  fourierdlem80  39079  caragenuncllem  39402  carageniuncllem1  39411  1fzopredsuc  39947  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  lmod1  42075
  Copyright terms: Public domain W3C validator