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

Theorem uneq1d 3758
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 3752 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  cun 3565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-un 3572
This theorem is referenced by:  ifeq1  4081  preq1  4259  tpeq1  4268  tpeq2  4269  tpprceq3  4326  iunxdif3  4597  iununi  4601  resasplit  6061  fresaunres2  6063  fmptpr  6423  funresdfunsn  6440  ressuppssdif  7301  sbthlem5  8059  fodomr  8096  domunfican  8218  brwdom2  8463  cdaval  8977  ackbij1lem2  9028  ttukeylem3  9318  snunioo  12283  snunioc  12285  prunioo  12286  fzpred  12374  fseq1p1m1  12398  nn0split  12438  fz0sn0fz1  12440  fzo0sn0fzo1  12541  fzosplitprm1  12561  s2prop  13633  s4prop  13636  fsum1p  14463  fprod1p  14679  setsval  15869  setsabs  15883  setscom  15884  prdsval  16096  prdsdsval  16119  prdsdsval2  16125  prdsdsval3  16126  mreexexlem3d  16287  mreexexlem4d  16288  estrres  16760  symg2bas  17799  evlseu  19497  ordtuni  20975  lfinun  21309  alexsubALTlem3  21834  ustssco  21999  trust  22014  ressprdsds  22157  xpsdsval  22167  nulmbl2  23285  uniioombllem3  23334  uniioombllem4  23335  plyeq0  23948  plyaddlem1  23950  plymullem1  23951  fta1lem  24043  vieta1lem2  24047  birthdaylem2  24660  edglnl  26019  iuninc  29351  difelcarsg  30346  actfunsnf1o  30656  reprsuc  30667  breprexplema  30682  bnj1416  31081  mclsval  31434  mclsax  31440  rankung  32248  topjoin  32335  bj-tageq  32939  finixpnum  33365  poimirlem3  33383  poimirlem4  33384  poimirlem6  33386  poimirlem7  33387  poimirlem9  33389  poimirlem16  33396  poimirlem17  33397  poimirlem28  33408  mblfinlem2  33418  islshpsm  34086  lshpnel2N  34091  lkrlsp3  34210  pclfinclN  35055  dochsatshp  36559  mapfzcons1  37099  iunrelexp0  37813  isotone1  38166  fiiuncl  39054  nnsplit  39387  fourierdlem32  40119  fzopred  41095  fzopredsuc  41096  fzosplitpr  41102  aacllem  42312
  Copyright terms: Public domain W3C validator