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

Theorem uneq1i 3596
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 3593 . 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 1455    u. cun 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421
This theorem is referenced by:  un12  3604  unundi  3607  undif1  3854  dfif5  3909  tpcoma  4081  qdass  4084  qdassr  4085  tpidm12  4086  symdifv  4370  unidif0  4590  difxp2  5282  resasplit  5776  fresaun  5777  fresaunres2  5778  df2o3  7221  sbthlem6  7713  fodomr  7749  domss2  7757  domunfican  7870  kmlem11  8616  hashfun  12642  prmreclem2  14910  setscom  15202  gsummptfzsplitl  17615  uniioombllem3  22592  lhop  23017  usgrafilem1  25188  constr3pthlem1  25432  ex-un  25923  ex-pw  25928  indifundif  28201  bnj1415  29896  subfacp1lem1  29951  dftrpred4g  30524  lineunray  30963  bj-2upln1upl  31663  poimirlem3  31988  poimirlem4  31989  poimirlem5  31990  poimirlem16  32001  poimirlem17  32002  poimirlem19  32004  poimirlem20  32005  poimirlem22  32007  dfrcl2  36311  iunrelexp0  36339  trclfvdecomr  36365  corcltrcl  36376  cotrclrcl  36379  fourierdlem80  38088  caragenuncllem  38371  carageniuncllem1  38380  1fzopredsuc  38759  nnsum4primeseven  38933  nnsum4primesevenALTV  38934  usgfislem1  40029  usgfisALTlem1  40033  lmod1  40558
  Copyright terms: Public domain W3C validator