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

Theorem uneq1d 3964
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 3958 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1653  cun 3767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-v 3387  df-un 3774
This theorem is referenced by:  ifeq1  4281  preq1  4457  tpeq1  4466  tpeq2  4467  tpprceq3  4523  iunxdif3  4797  iununi  4801  resasplit  6289  fresaunres2  6291  fmptpr  6667  funresdfunsn  6684  ressuppssdif  7553  sbthlem5  8316  fodomr  8353  domunfican  8475  brwdom2  8720  cdaval  9280  ackbij1lem2  9331  ttukeylem3  9621  snunioo  12552  snunioc  12554  prunioo  12555  fzpred  12643  fseq1p1m1  12668  nn0split  12709  fz0sn0fz1  12711  fzo0sn0fzo1  12812  fzosplitpr  12832  s2prop  13992  s4prop  13995  fsum1p  14823  fprod1p  15035  setsval  16214  setsabs  16227  setscom  16228  prdsval  16430  prdsdsval  16453  prdsdsval2  16459  prdsdsval3  16460  mreexexlem3d  16621  mreexexlem4d  16622  estrresOLD  17093  estrres  17094  symg2bas  18130  evlseu  19838  ordtuni  21323  lfinun  21657  alexsubALTlem3  22181  ustssco  22346  trust  22361  ressprdsds  22504  xpsdsval  22514  nulmbl2  23644  uniioombllem3  23693  uniioombllem4  23694  plyeq0  24308  plyaddlem1  24310  plymullem1  24311  fta1lem  24403  vieta1lem2  24407  birthdaylem2  25031  edglnl  26379  iuninc  29896  difelcarsg  30888  actfunsnf1o  31202  reprsuc  31213  breprexplema  31228  bnj1416  31624  mclsval  31977  mclsax  31983  rankung  32786  topjoin  32872  bj-tageq  33456  finixpnum  33883  poimirlem3  33901  poimirlem4  33902  poimirlem6  33904  poimirlem7  33905  poimirlem9  33907  poimirlem16  33914  poimirlem17  33915  poimirlem28  33926  mblfinlem2  33936  islshpsm  35001  lshpnel2N  35006  lkrlsp3  35125  pclfinclN  35971  dochsatshp  37472  mapfzcons1  38066  iunrelexp0  38777  isotone1  39128  fiiuncl  39993  nnsplit  40318  fourierdlem32  41099  fzopred  42172  fzopredsuc  42173  aacllem  43349
  Copyright terms: Public domain W3C validator