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

Theorem uneq1i 3559
Description: Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
uneq1i.1  |-  A  =  B
Assertion
Ref Expression
uneq1i  |-  ( A  u.  C )  =  ( B  u.  C
)

Proof of Theorem uneq1i
StepHypRef Expression
1 uneq1i.1 . 2  |-  A  =  B
2 uneq1 3556 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
31, 2ax-mp 5 1  |-  ( A  u.  C )  =  ( B  u.  C
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    u. cun 3377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-un 3384
This theorem is referenced by:  un12  3567  unundi  3570  undif1  3815  dfif5  3870  tpcoma  4039  qdass  4042  qdassr  4043  tpidm12  4044  symdifv  4320  unidif0  4540  difxp2  5225  resasplit  5713  fresaun  5714  fresaunres2  5715  df2o3  7150  sbthlem6  7640  fodomr  7676  domss2  7684  domunfican  7797  kmlem11  8541  hashfun  12557  prmreclem2  14804  setscom  15096  gsummptfzsplitl  17509  uniioombllem3  22485  lhop  22910  usgrafilem1  25081  constr3pthlem1  25325  ex-un  25816  ex-pw  25821  indifundif  28095  bnj1415  29799  subfacp1lem1  29854  dftrpred4g  30426  lineunray  30863  bj-2upln1upl  31529  poimirlem3  31850  poimirlem4  31851  poimirlem5  31852  poimirlem16  31863  poimirlem17  31864  poimirlem19  31866  poimirlem20  31867  poimirlem22  31869  dfrcl2  36179  iunrelexp0  36207  trclfvdecomr  36233  corcltrcl  36244  cotrclrcl  36247  fourierdlem80  37933  caragenuncllem  38184  carageniuncllem1  38193  1fzopredsuc  38534  nnsum4primeseven  38708  nnsum4primesevenALTV  38709  usgfislem1  39357  usgfisALTlem1  39361  lmod1  39888
  Copyright terms: Public domain W3C validator