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

Theorem uneq1d 4124
 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 4118 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∪ cun 3917 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924 This theorem is referenced by:  ifeq1  4454  preq1  4654  tpeq1  4663  tpeq2  4664  tpprceq3  4721  iunxdif3  5003  iununi  5007  resasplit  6538  fresaunres2  6540  fmptpr  6925  funresdfunsn  6942  ressuppssdif  7847  sbthlem5  8628  fodomr  8665  domunfican  8788  brwdom2  9034  ackbij1lem2  9641  ttukeylem3  9931  snunioo  12865  snunioc  12867  prunioo  12868  fzpred  12959  fseq1p1m1  12985  nn0split  13026  fz0sn0fz1  13028  fzo0sn0fzo1  13130  fzosplitpr  13150  s2prop  14269  s4prop  14272  fsum1p  15108  fprod1p  15322  setsval  16513  setsabs  16526  setscom  16527  prdsval  16728  prdsdsval  16751  prdsdsval2  16757  prdsdsval3  16758  mreexexlem3d  16917  mreexexlem4d  16918  estrres  17389  symg2bas  18521  symgvalstruct  18525  evlseu  20762  ordtuni  21801  lfinun  22136  alexsubALTlem3  22660  ustssco  22826  trust  22841  ressprdsds  22984  xpsdsval  22994  nulmbl2  24146  uniioombllem3  24195  uniioombllem4  24196  plyeq0  24814  plyaddlem1  24816  plymullem1  24817  fta1lem  24909  vieta1lem2  24913  birthdaylem2  25544  edglnl  26942  iuninc  30326  pmtrcnel2  30769  tocycval  30785  cycpmco2rn  30802  difelcarsg  31628  actfunsnf1o  31935  reprsuc  31946  breprexplema  31961  bnj1416  32371  mclsval  32870  mclsax  32876  rankung  33687  topjoin  33773  bj-tageq  34359  finixpnum  34990  poimirlem3  35008  poimirlem4  35009  poimirlem6  35011  poimirlem7  35012  poimirlem9  35014  poimirlem16  35021  poimirlem17  35022  poimirlem28  35033  mblfinlem2  35043  islshpsm  36224  lshpnel2N  36229  lkrlsp3  36348  pclfinclN  37194  dochsatshp  38695  metakunt24  39322  mapfzcons1  39578  iunrelexp0  40323  isotone1  40674  fiiuncl  41623  nnsplit  41920  fourierdlem32  42711  fzopred  43809  fzopredsuc  43810  aacllem  45259
 Copyright terms: Public domain W3C validator