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

Theorem uneq1d 3656
Description: Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.)
Hypothesis
Ref Expression
uneq1d.1
Assertion
Ref Expression
uneq1d

Proof of Theorem uneq1d
StepHypRef Expression
1 uneq1d.1 . 2
2 uneq1 3650 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  u.cun 3473
This theorem is referenced by:  ifeq1  3945  preq1  4109  tpeq1  4118  tpeq2  4119  tpprceq3  4170  iununi  4415  resasplit  5760  fresaunres2  5762  fmptpr  6096  funresdfunsn  6113  ressuppssdif  6940  sbthlem5  7651  fodomr  7688  domunfican  7813  brwdom2  8020  cdaval  8571  ackbij1lem2  8622  ttukeylem3  8912  snunioo  11675  snunioc  11677  prunioo  11678  fzpred  11757  fseq1p1m1  11781  nn0split  11819  fzo0sn0fzo1  11902  fzosplitprm1  11919  s2prop  12862  s4prop  12863  fsum1p  13568  fprod1p  13772  setsval  14656  setsabs  14661  setscom  14662  prdsval  14852  prdsdsval  14875  prdsdsval2  14881  prdsdsval3  14882  mreexexlem3d  15043  mreexexlem4d  15044  symg2bas  16423  evlseu  18185  ordtuni  19691  lfinun  20026  alexsubALTlem3  20549  ustssco  20717  trust  20732  ressprdsds  20874  xpsdsval  20884  nulmbl2  21947  uniioombllem3  21994  uniioombllem4  21995  plyeq0  22608  plyaddlem1  22610  plymullem1  22611  fta1lem  22703  vieta1lem2  22707  birthdaylem2  23282  nbgraopALT  24424  iuninc  27428  mclsval  28923  mclsax  28929  rankung  29823  finixpnum  30038  mblfinlem2  30052  topjoin  30183  mapfzcons1  30649  fourierdlem32  31921  fzosplitpr  32342  estrres  32645  aacllem  33216  bnj1416  34095  bj-tageq  34534  islshpsm  34705  lshpnel2N  34710  lkrlsp3  34829  pclfinclN  35674  dochsatshp  37178
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480
  Copyright terms: Public domain W3C validator