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

Theorem uneq2d 3342
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 3336 . 2  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
31, 2syl 15 1  |-  ( ph  ->  ( C  u.  A
)  =  ( C  u.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    u. cun 3163
This theorem is referenced by:  ifeq2  3583  tpeq3  3730  iununi  4002  relcoi1  5217  resasplit  5427  fvun1  5606  fvunsn  5728  fnsnsplit  5733  oev2  6538  oarec  6576  sbthlem5  6991  sbthlem6  6992  domss2  7036  domunfican  7145  fiint  7149  fodomfi  7151  pm54.43  7649  kmlem2  7793  kmlem11  7802  cdaval  7812  cdaassen  7824  ackbij1lem1  7862  fin23lem26  7967  axdc3lem4  8095  fpwwe2lem13  8280  wunex2  8376  wuncval2  8385  snunico  10779  ioojoin  10782  fzsuc  10851  fseq1p1m1  10873  fseq1m1p1  10874  fzosplitsn  10936  hashfun  11405  fsumm1  12232  climcndslem1  12324  ruclem4  12528  vdwap1  13040  setscom  13192  mreexmrid  13561  mreexexlemd  13562  mreexexlem2d  13563  cnvtsr  14347  dprd2da  15293  dmdprdsplit2lem  15296  lspun0  15784  lbsextlem4  15930  cmpcld  17145  trfil2  17598  cldsubg  17809  tsmsres  17842  icccmplem2  18344  uniioombllem4  18957  ppiprm  20405  chtprm  20407  pntrsumbnd2  20732  fzspl  23046  ballotlemfp1  23066  fmptapd  23228  subfacp1lem1  23725  cvmscld  23819  eupath2lem3  23918  rankaltopb  24585  rankung  24868  isconc1  26109  isconc2  26110  isconc3  26111  clscnc  26113  comppfsc  26410  fndifnfp  26859  ralxpmap  26864  diophren  26999  stoweidlem11  27863  stoweidlem26  27878  s4prop  28222  bnj941  29120  bnj944  29286  lshpnel2N  29797  paddfval  30608  hdmapval  32643
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170
  Copyright terms: Public domain W3C validator