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

Theorem uneq1i 3927
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 3924 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1652  cun 3732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-un 3739
This theorem is referenced by:  un12  3935  unundi  3938  undif1  4205  dfif5  4261  tpcoma  4442  qdass  4445  qdassr  4446  tpidm12  4447  symdifv  4756  unidif0  4998  difxp2  5745  resasplit  6258  fresaun  6259  fresaunres2  6260  df2o3  7780  sbthlem6  8284  fodomr  8320  domss2  8328  domunfican  8442  kmlem11  9237  hashfun  13428  prmreclem2  15903  setscom  16178  gsummptfzsplitl  18602  uniioombllem3  23646  lhop  24073  ex-un  27743  ex-pw  27748  indifundif  29808  bnj1415  31557  subfacp1lem1  31612  dftrpred4g  32180  lineunray  32701  bj-2upln1upl  33442  poimirlem3  33839  poimirlem4  33840  poimirlem5  33841  poimirlem16  33852  poimirlem17  33853  poimirlem19  33855  poimirlem20  33856  poimirlem22  33858  dfrcl2  38644  iunrelexp0  38672  trclfvdecomr  38698  corcltrcl  38709  cotrclrcl  38712  df3o2  38999  fourierdlem80  41043  caragenuncllem  41369  carageniuncllem1  41378  1fzopredsuc  42071  nnsum4primeseven  42367  nnsum4primesevenALTV  42368  lmod1  42953
  Copyright terms: Public domain W3C validator