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

Theorem uneq1d 3909
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 3903 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  cun 3713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-un 3720
This theorem is referenced by:  ifeq1  4234  preq1  4412  tpeq1  4421  tpeq2  4422  tpprceq3  4480  iunxdif3  4758  iununi  4762  resasplit  6235  fresaunres2  6237  fmptpr  6602  funresdfunsn  6619  ressuppssdif  7484  sbthlem5  8239  fodomr  8276  domunfican  8398  brwdom2  8643  cdaval  9184  ackbij1lem2  9235  ttukeylem3  9525  snunioo  12491  snunioc  12493  prunioo  12494  fzpred  12582  fseq1p1m1  12607  nn0split  12648  fz0sn0fz1  12650  fzo0sn0fzo1  12751  fzosplitpr  12771  s2prop  13852  s4prop  13855  fsum1p  14681  fprod1p  14897  setsval  16090  setsabs  16104  setscom  16105  prdsval  16317  prdsdsval  16340  prdsdsval2  16346  prdsdsval3  16347  mreexexlem3d  16508  mreexexlem4d  16509  estrres  16980  symg2bas  18018  evlseu  19718  ordtuni  21196  lfinun  21530  alexsubALTlem3  22054  ustssco  22219  trust  22234  ressprdsds  22377  xpsdsval  22387  nulmbl2  23504  uniioombllem3  23553  uniioombllem4  23554  plyeq0  24166  plyaddlem1  24168  plymullem1  24169  fta1lem  24261  vieta1lem2  24265  birthdaylem2  24878  edglnl  26237  iuninc  29686  difelcarsg  30681  actfunsnf1o  30991  reprsuc  31002  breprexplema  31017  bnj1416  31414  mclsval  31767  mclsax  31773  rankung  32579  topjoin  32666  bj-tageq  33270  finixpnum  33707  poimirlem3  33725  poimirlem4  33726  poimirlem6  33728  poimirlem7  33729  poimirlem9  33731  poimirlem16  33738  poimirlem17  33739  poimirlem28  33750  mblfinlem2  33760  islshpsm  34770  lshpnel2N  34775  lkrlsp3  34894  pclfinclN  35739  dochsatshp  37242  mapfzcons1  37782  iunrelexp0  38496  isotone1  38848  fiiuncl  39733  nnsplit  40072  fourierdlem32  40859  fzopred  41842  fzopredsuc  41843  aacllem  43060
  Copyright terms: Public domain W3C validator