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

Theorem unieqd 4222
Description: Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)
Hypothesis
Ref Expression
unieqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
unieqd  |-  ( ph  ->  U. A  =  U. B )

Proof of Theorem unieqd
StepHypRef Expression
1 unieqd.1 . 2  |-  ( ph  ->  A  =  B )
2 unieq 4220 . 2  |-  ( A  =  B  ->  U. A  =  U. B )
31, 2syl 17 1  |-  ( ph  ->  U. A  =  U. B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455   U.cuni 4212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rex 2755  df-uni 4213
This theorem is referenced by:  uniprg  4226  unisng  4228  unisn3  4229  csbuni  4240  unisn2  4555  opswap  5346  unixpid  5394  iotaeq  5577  iotabi  5578  uniabio  5579  iotanul  5584  funfv  5960  funfv2  5961  fvun  5963  dffv2  5966  fniunfv  6182  ordunisuc  6691  orduniss2  6692  onsucuni2  6693  elxp4  6769  elxp5  6770  1stval  6827  2ndval  6828  1stnpr  6829  2ndnpr  6830  fo1st  6845  fo2nd  6846  f1stres  6847  f2ndres  6848  1st2val  6851  2nd2val  6852  2nd1st  6870  cnvf1olem  6926  brtpos2  7010  dftpos4  7023  tpostpos  7024  wrecseq123  7060  tz7.44-2  7156  tz7.44-3  7157  rdglim2  7181  ixpsnf1o  7593  xpcomco  7693  xpassen  7697  xpdom2  7698  supeq1  7990  supeq2  7993  supeq3  7994  supeq123d  7995  supval2  8000  rankuni  8365  en2other2  8471  dfac2a  8591  dfac12lem1  8604  dfac12r  8607  kmlem9  8619  kmlem11  8621  kmlem12  8622  enfin2i  8782  fin23lem29  8802  fin23lem30  8803  fin23lem32  8805  fin23lem34  8807  fin23lem35  8808  fin23lem36  8809  fin23lem38  8810  fin23lem39  8811  fin23lem41  8813  isf34lem7  8840  isf34lem6  8841  fin1a2lem10  8870  fin1a2lem11  8871  fin1a2lem12  8872  itunisuc  8880  itunitc  8882  ttukeylem3  8972  ttukey2g  8977  pwcfsdom  9039  gruurn  9254  dfinfre  10621  dfinfmrOLD  10622  relexpfld  13167  fsumcnv  13889  fprodcnv  14092  mrcun  15583  isacs1i  15618  mreacs  15619  arwval  15993  ipoval  16455  isacs5lem  16470  acsdrscl  16471  acsficl  16472  isps  16503  isdir  16533  pmtrval  17147  pmtrfv  17148  pmtrprfv  17149  pmtrdifellem3  17174  pmtrprfval  17183  gsumcom2  17662  dmdprd  17685  dprddisj  17696  dprdf1o  17720  dprdsn  17724  dprd2da  17730  dprd2db  17731  dmdprdsplit2lem  17733  lspuni0  18288  lss0v  18294  zrhval  19134  zrhval2  19135  zrhpropd  19141  isbasisg  20017  basis1  20020  baspartn  20024  tgval  20025  eltg  20027  ntrfval  20094  ntrval  20106  tgrest  20230  restuni2  20238  lmfval  20303  cnfval  20304  cnpfval  20305  pnrmopn  20414  fiuncmp  20474  cmpfi  20478  ptval  20640  ptpjpre1  20641  elptr2  20644  ptuni2  20646  ptbasin  20647  ptbasfi  20651  xkoval  20657  txtopon  20661  ptuni  20664  ptunimpt  20665  xkouni  20669  ptpjcn  20681  ptcld  20683  dfac14  20688  ptcnp  20692  prdstopn  20698  ptrescn  20709  txcmplem2  20712  xkoptsub  20724  xkopt  20725  qtopval  20765  qtopeu  20786  hmphindis  20867  txswaphmeolem  20874  ptuncnv  20877  ptunhmeo  20878  xpstopnlem1  20879  flimval  21033  fcfval  21103  alexsubALTlem3  21119  ptcmplem1  21122  ptcmplem2  21123  ptcmplem3  21124  ptcmplem4  21125  ptcmpg  21127  cnextfres1  21138  cldsubg  21180  utopval  21302  tusval  21336  tuslem  21337  tususs  21340  ucnval  21347  prdsxmslem2  21599  ishtpy  22058  pi1buni  22126  pi1xfrcnv  22143  elovolmr  22484  ovoliunlem3  22512  uniioombllem2  22596  uniioombllem2OLD  22597  uniioombllem3  22599  dyadmbl  22614  vmaval  24096  vmappw  24099  disjabrex  28246  disjabrexf  28247  fcnvgreu  28327  xrge0tsmseq  28601  locfinreflem  28718  locfinref  28719  pstmval  28749  pstmfval  28750  ordtprsuni  28776  esumeq12dvaf  28903  esumeq2  28908  esumval  28918  esumf1o  28922  esumsnf  28936  esumss  28944  esumpfinval  28947  esumpfinvalf  28948  sigapildsys  29035  sxsigon  29065  meascnbl  29092  brae  29114  braew  29115  faeval  29119  imambfm  29134  cnmbfm  29135  dya2iocuni  29155  omsval  29167  omsfval  29168  omsf  29170  omsvalOLD  29171  omsfvalOLD  29172  omsfOLD  29174  oms0  29175  omssubaddlem  29177  omssubadd  29178  oms0OLD  29179  omssubaddlemOLD  29181  omssubaddOLD  29182  carsgval  29185  carsgclctunlem3  29202  omsmeas  29205  omsmeasOLD  29206  elprob  29292  probfinmeasb  29312  probmeasb  29313  dstrvprob  29354  indispcon  30007  iscvm  30032  cvmscld  30046  msrfval  30225  msrval  30226  mthmpps  30270  rdgprc0  30490  rdgprc  30491  dfrdg2  30492  dfrdg3  30493  trpredeq1  30511  trpredeq2  30512  trpredeq3  30513  nofulllem1  30641  nofulllem2  30642  unisnif  30742  brapply  30755  isfne  31045  fnemeet2  31073  fnejoin2  31075  tailfval  31078  ordcmp  31157  csbwrecsg  31774  mptsnunlem  31786  dissneqlem  31788  ptrest  31985  mblfinlem2  32024  ovoliunnfl  32028  voliunnfl  32030  volsupnfl  32031  mapdunirnN  35264  aomclem8  35965  dfac21  35970  csbfv12gALTOLD  37254  stoweidlem39  38001  salgenuni  38297  caragenval  38422  isome  38423  omeiunle  38446  isomennd  38460  unidmovn  38542  rrnmbl  38543  unidmvon  38546  hspmbl  38558  ovolval4lem2  38579  ovolval5lem2  38582  ovolval5lem3  38583  ovolval5  38584  ovnovollem2  38586
  Copyright terms: Public domain W3C validator