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

Theorem uneq2d 3800
Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
Hypothesis
Ref Expression
uneq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
uneq2d (𝜑 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem uneq2d
StepHypRef Expression
1 uneq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 uneq2 3794 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  cun 3605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612
This theorem is referenced by:  ifeq2  4124  tpeq3  4311  iununi  4642  sucprc  5838  resasplit  6112  fvun1  6308  fmptapd  6478  fndifnfp  6483  fvunsn  6486  fnsnsplit  6491  oev2  7648  oarec  7687  ralxpmap  7949  sbthlem5  8115  sbthlem6  8116  domss2  8160  domunfican  8274  fiint  8278  fodomfi  8280  pm54.43  8864  kmlem2  9011  kmlem11  9020  cdaval  9030  cdaassen  9042  ackbij1lem1  9080  fin23lem26  9185  axdc3lem4  9313  fpwwe2lem13  9502  wunex2  9598  wuncval2  9607  snunico  12337  ioojoin  12341  fzsuc  12426  fseq1p1m1  12452  fseq1m1p1  12453  fzosplitsnm1  12582  fzosplitsn  12616  fzosplitpr  12617  fzosplitprm1  12618  hashfun  13262  resunimafz0  13267  s4prop  13701  fsumm1  14524  climcndslem1  14625  fprodm1  14741  ruclem4  15007  lcmfunsnlem1  15397  lcmfunsnlem2lem1  15398  lcmfunsnlem2lem2  15399  lcmfunsnlem2  15400  lcmfunsn  15404  vdwap1  15728  setsidvald  15936  setscom  15950  mreexmrid  16350  mreexexlemd  16351  mreexexlem2d  16352  cnvtsr  17269  dprd2da  18487  dmdprdsplit2lem  18490  lspun0  19059  lbsextlem4  19209  cmpcld  21253  comppfsc  21383  trfil2  21738  cldsubg  21961  tsmsres  21994  icccmplem2  22673  uniioombllem4  23400  ppiprm  24922  chtprm  24924  pntrsumbnd2  25301  pthdlem1  26718  wwlksnext  26856  clwwlknonex2lem1  27082  difres  29539  ofpreima2  29594  fzspl  29678  ordtprsuni  30093  ordtcnvNEW  30094  carsgsigalem  30505  ballotlemfp1  30681  fsum2dsub  30813  reprsuc  30821  bnj941  30969  bnj944  31134  subfacp1lem1  31287  cvmscld  31381  mrsubvrs  31545  mclsval  31586  noextend  31944  nodenselem5  31963  nosupbnd2lem1  31986  rankaltopb  32211  rankung  32398  lindsenlbs  33534  poimirlem1  33540  poimirlem2  33541  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem13  33552  poimirlem14  33553  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem26  33565  poimirlem28  33567  poimirlem31  33570  poimirlem32  33571  lshpnel2N  34590  paddfval  35401  hdmapval  37437  diophren  37694  ioounsn  38112  iunrelexp0  38311  trclfvdecoml  38338  isotone1  38663  iunp1  39549  snunioo2  40049  snunioo1  40056  dvmptfprodlem  40477  stoweidlem11  40546  stoweidlem26  40561  fourierdlem33  40675  fzopredsuc  41658  iccpartltu  41686  iccpartgt  41688  lmod1zr  42607
  Copyright terms: Public domain W3C validator