MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uneq2d Structured version   Unicode version

Theorem uneq2d 3498
Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
Hypothesis
Ref Expression
uneq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
uneq2d  |-  ( ph  ->  ( C  u.  A
)  =  ( C  u.  B ) )

Proof of Theorem uneq2d
StepHypRef Expression
1 uneq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 uneq2 3492 . 2  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
31, 2syl 16 1  |-  ( ph  ->  ( C  u.  A
)  =  ( C  u.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    u. cun 3314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321
This theorem is referenced by:  ifeq2  3784  tpeq3  3953  iununi  4243  relcoi1  5354  resasplit  5569  fvun1  5750  fmptapd  5889  fndifnfp  5894  fvunsn  5897  fnsnsplit  5902  oev2  6951  oarec  6989  ralxpmap  7250  sbthlem5  7413  sbthlem6  7414  domss2  7458  domunfican  7572  fiint  7576  fodomfi  7578  pm54.43  8158  kmlem2  8308  kmlem11  8317  cdaval  8327  cdaassen  8339  ackbij1lem1  8377  fin23lem26  8482  axdc3lem4  8610  fpwwe2lem13  8796  wunex2  8892  wuncval2  8901  snunico  11398  ioojoin  11402  fzsuc  11488  fseq1p1m1  11517  fseq1m1p1  11518  fzosplitsnm1  11591  fzosplitsn  11616  hashfun  12182  s4prop  12508  fsumm1  13203  climcndslem1  13294  ruclem4  13498  vdwap1  14020  setscom  14186  mreexmrid  14563  mreexexlemd  14564  mreexexlem2d  14565  cnvtsr  15374  dprd2da  16514  dmdprdsplit2lem  16517  lspun0  17013  lbsextlem4  17163  cmpcld  18846  trfil2  19301  cldsubg  19522  tsmsresOLD  19558  tsmsres  19559  icccmplem2  20241  uniioombllem4  20907  ppiprm  22373  chtprm  22375  pntrsumbnd2  22700  eupath2lem3  23422  ofpreima2  25808  fzspl  25899  ordtprsuni  26202  ballotlemfp1  26721  subfacp1lem1  26914  cvmscld  27009  fprodm1  27323  rankaltopb  27856  rankung  28050  comppfsc  28420  diophren  28994  ioounsn  29427  stoweidlem11  29649  stoweidlem26  29664  fzosplitpr  30066  fzosplitprm1  30067  wwlknext  30199  lmod1zr  30741  bnj941  31465  bnj944  31630  lshpnel2N  32200  paddfval  33011  hdmapval  35046
  Copyright terms: Public domain W3C validator