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

Theorem uneq1d 3727
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 3721 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  cun 3537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544
This theorem is referenced by:  ifeq1  4039  preq1  4211  tpeq1  4220  tpeq2  4221  tpprceq3  4275  iunxdif3  4536  iununi  4540  resasplit  5972  fresaunres2  5974  fmptpr  6321  funresdfunsn  6338  ressuppssdif  7180  sbthlem5  7936  fodomr  7973  domunfican  8095  brwdom2  8338  cdaval  8852  ackbij1lem2  8903  ttukeylem3  9193  snunioo  12125  snunioc  12127  prunioo  12128  fzpred  12214  fseq1p1m1  12238  nn0split  12278  fz0sn0fz1  12280  fzo0sn0fzo1  12379  fzosplitprm1  12398  s2prop  13448  s4prop  13451  fsum1p  14272  fprod1p  14483  setsval  15666  setsabs  15676  setscom  15677  prdsval  15884  prdsdsval  15907  prdsdsval2  15913  prdsdsval3  15914  mreexexlem3d  16075  mreexexlem4d  16076  estrres  16548  symg2bas  17587  evlseu  19283  ordtuni  20746  lfinun  21080  alexsubALTlem3  21605  ustssco  21770  trust  21785  ressprdsds  21927  xpsdsval  21937  nulmbl2  23028  uniioombllem3  23076  uniioombllem4  23077  plyeq0  23688  plyaddlem1  23690  plymullem1  23691  fta1lem  23783  vieta1lem2  23787  birthdaylem2  24396  nbgraopALT  25719  iuninc  28567  difelcarsg  29505  bnj1416  30167  mclsval  30520  mclsax  30526  rankung  31249  topjoin  31336  bj-tageq  31960  finixpnum  32367  poimirlem3  32385  poimirlem4  32386  poimirlem6  32388  poimirlem7  32389  poimirlem9  32391  poimirlem16  32398  poimirlem17  32399  poimirlem28  32410  mblfinlem2  32420  islshpsm  33088  lshpnel2N  33093  lkrlsp3  33212  pclfinclN  34057  dochsatshp  35561  mapfzcons1  36101  iunrelexp0  36816  isotone1  37169  fiiuncl  38062  nnsplit  38319  fourierdlem32  38836  fzopred  39750  fzopredsuc  39751  fzosplitpr  40189  aacllem  42319
  Copyright terms: Public domain W3C validator