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

Theorem uneq1i 3620
 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 3617 . 2
31, 2ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1370  u.cun 3440 This theorem is referenced by:  un12  3628  unundi  3631  undif1  3868  dfif5  3921  tpcoma  4088  qdass  4091  qdassr  4092  tpidm12  4093  unidif0  4582  difxp2  5383  resasplit  5703  fresaun  5704  fresaunres2  5705  fmptpr  6028  df2o3  7067  sbthlem6  7560  fodomr  7596  domss2  7604  domunfican  7719  kmlem11  8466  hashfun  12357  prmreclem2  14136  setscom  14362  gsummptfzsplitl  16588  uniioombllem3  21465  lhop  21888  usgrafilem1  23793  constr3pthlem1  24010  ex-un  24100  ex-pw  24105  subfacp1lem1  27523  dftrpred4g  28154  symdifV  28312  lineunray  28634  fourierdlem80  30716  lmod1  31806  bnj1415  32872  bj-2upln1upl  33362 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3083  df-un 3447
 Copyright terms: Public domain W3C validator