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

Theorem uneq2d 3556
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 3550 . 2  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
31, 2syl 17 1  |-  ( ph  ->  ( C  u.  A
)  =  ( C  u.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1448    u. cun 3370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-v 3015  df-un 3377
This theorem is referenced by:  ifeq2  3854  tpeq3  4031  iununi  4338  relcoi1OLD  5344  resasplit  5736  fvun1  5920  fmptapd  6073  fndifnfp  6078  fvunsn  6081  fnsnsplit  6086  oev2  7212  oarec  7250  ralxpmap  7508  sbthlem5  7673  sbthlem6  7674  domss2  7718  domunfican  7831  fiint  7835  fodomfi  7837  pm54.43  8421  kmlem2  8568  kmlem11  8577  cdaval  8587  cdaassen  8599  ackbij1lem1  8637  fin23lem26  8742  axdc3lem4  8870  fpwwe2lem13  9054  wunex2  9150  wuncval2  9159  snunico  11750  ioojoin  11754  fzsuc  11834  fseq1p1m1  11859  fseq1m1p1  11860  fzosplitsnm1  11981  fzosplitsn  12010  fzosplitprm1  12011  hashfun  12604  s4prop  13003  fsumm1  13823  climcndslem1  13918  fprodm1  14032  ruclem4  14297  lcmfunsnlem1  14621  lcmfunsnlem2lem1  14622  lcmfunsnlem2lem2  14623  lcmfunsnlem2  14624  lcmfunsn  14628  vdwap1  14938  setsidvald  15158  setscom  15164  mreexmrid  15560  mreexexlemd  15561  mreexexlem2d  15562  cnvtsr  16479  dprd2da  17686  dmdprdsplit2lem  17689  lspun0  18245  lbsextlem4  18395  cmpcld  20428  comppfsc  20558  trfil2  20913  cldsubg  21136  tsmsres  21169  icccmplem2  21852  uniioombllem4  22556  ppiprm  24090  chtprm  24092  pntrsumbnd2  24417  wwlknext  25464  eupath2lem3  25719  difres  28220  ofpreima2  28277  fzspl  28376  ordtprsuni  28732  ordtcnvNEW  28733  carsgsigalem  29153  ballotlemfp1  29330  bnj941  29590  bnj944  29755  subfacp1lem1  29908  cvmscld  30002  mrsubvrs  30166  mclsval  30207  rankaltopb  30752  rankung  30939  poimirlem1  31943  poimirlem2  31944  poimirlem4  31946  poimirlem6  31948  poimirlem7  31949  poimirlem8  31950  poimirlem13  31955  poimirlem14  31956  poimirlem16  31958  poimirlem17  31959  poimirlem18  31960  poimirlem19  31961  poimirlem20  31962  poimirlem21  31963  poimirlem22  31964  poimirlem26  31968  poimirlem28  31970  poimirlem31  31973  poimirlem32  31974  lshpnel2N  32553  paddfval  33364  hdmapval  35401  diophren  35658  ioounsn  36096  iunrelexp0  36296  trclfvdecoml  36323  iunp1  37402  snunioo2  37647  snunioo1  37654  dvmptfprodlem  37861  stoweidlem11  37928  stoweidlem26  37943  fourierdlem33  38060  fzopredsuc  38811  iccpartltu  38830  iccpartgt  38832  fzosplitpr  39159  pthdlem1  39844  lmod1zr  40611
  Copyright terms: Public domain W3C validator