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

Theorem unieqd 4478
Description: Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)
Hypothesis
Ref Expression
unieqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
unieqd (𝜑 𝐴 = 𝐵)

Proof of Theorem unieqd
StepHypRef Expression
1 unieqd.1 . 2 (𝜑𝐴 = 𝐵)
2 unieq 4476 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2syl 17 1 (𝜑 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523   cuni 4468
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-rex 2947  df-uni 4469
This theorem is referenced by:  uniprg  4482  unisng  4484  unisn3  4485  csbuni  4498  unisn2  4827  opswap  5660  unixpid  5708  iotaeq  5897  iotabi  5898  uniabio  5899  iotanul  5904  funfv  6304  funfv2  6305  fvun  6307  dffv2  6310  fniunfv  6545  ordunisuc  7074  orduniss2  7075  onsucuni2  7076  elxp4  7152  elxp5  7153  1stval  7212  2ndval  7213  1stnpr  7214  2ndnpr  7215  fo1st  7230  fo2nd  7231  f1stres  7234  f2ndres  7235  1st2val  7238  2nd2val  7239  2nd1st  7257  cnvf1olem  7320  brtpos2  7403  dftpos4  7416  tpostpos  7417  wrecseq123  7453  tz7.44-2  7548  tz7.44-3  7549  rdglim2  7573  ixpsnf1o  7990  xpcomco  8091  xpassen  8095  xpdom2  8096  supeq1  8392  supeq2  8395  supeq3  8396  supeq123d  8397  supval2  8402  rankuni  8764  en2other2  8870  dfac2a  8990  dfac12lem1  9003  dfac12r  9006  kmlem9  9018  kmlem11  9020  kmlem12  9021  enfin2i  9181  fin23lem29  9201  fin23lem30  9202  fin23lem32  9204  fin23lem34  9206  fin23lem35  9207  fin23lem36  9208  fin23lem38  9209  fin23lem39  9210  fin23lem41  9212  isf34lem7  9239  isf34lem6  9240  fin1a2lem10  9269  fin1a2lem11  9270  fin1a2lem12  9271  itunisuc  9279  itunitc  9281  ttukeylem3  9371  ttukey2g  9376  pwcfsdom  9443  gruurn  9658  dfinfre  11042  relexpfld  13833  fsumcnv  14548  fprodcnv  14757  mrcun  16329  isacs1i  16365  mreacs  16366  arwval  16740  ipoval  17201  isacs5lem  17216  acsdrscl  17217  acsficl  17218  isps  17249  isdir  17279  pmtrval  17917  pmtrfv  17918  pmtrprfv  17919  pmtrdifellem3  17944  pmtrprfval  17953  gsumcom2  18420  dmdprd  18443  dprddisj  18454  dprdf1o  18477  dprdsn  18481  dprd2da  18487  dprd2db  18488  dmdprdsplit2lem  18490  lspuni0  19058  lss0v  19064  zrhval  19904  zrhval2  19905  zrhpropd  19911  isbasisg  20799  basis1  20802  baspartn  20806  tgval  20807  eltg  20809  ntrfval  20876  ntrval  20888  tgrest  21011  restuni2  21019  lmfval  21084  cnfval  21085  cnpfval  21086  pnrmopn  21195  fiuncmp  21255  cmpfi  21259  ptval  21421  ptpjpre1  21422  elptr2  21425  ptuni2  21427  ptbasin  21428  ptbasfi  21432  xkoval  21438  txtopon  21442  ptuni  21445  ptunimpt  21446  xkouni  21450  ptpjcn  21462  ptcld  21464  dfac14  21469  ptcnp  21473  prdstopn  21479  ptrescn  21490  txcmplem2  21493  xkoptsub  21505  xkopt  21506  qtopval  21546  qtopeu  21567  hmphindis  21648  txswaphmeolem  21655  ptuncnv  21658  ptunhmeo  21659  xpstopnlem1  21660  flimval  21814  fcfval  21884  alexsubALTlem3  21900  ptcmplem1  21903  ptcmplem2  21904  ptcmplem3  21905  ptcmplem4  21906  ptcmpg  21908  cnextfres1  21919  cldsubg  21961  utopval  22083  tusval  22117  tuslem  22118  tususs  22121  ucnval  22128  prdsxmslem2  22381  ishtpy  22818  pi1buni  22886  pi1xfrcnv  22903  elovolmr  23290  ovoliunlem3  23318  uniioombllem2  23397  uniioombllem3  23399  dyadmbl  23414  vmaval  24884  vmappw  24887  disjabrex  29521  disjabrexf  29522  fcnvgreu  29600  xrge0tsmseq  29915  locfinreflem  30035  locfinref  30036  pstmval  30066  pstmfval  30067  ordtprsuni  30093  esumeq12dvaf  30221  esumeq2  30226  esumval  30236  esumf1o  30240  esumsnf  30254  esumss  30262  esumpfinval  30265  esumpfinvalf  30266  sigapildsys  30353  sxsigon  30383  meascnbl  30410  brae  30432  braew  30433  faeval  30437  imambfm  30452  cnmbfm  30453  dya2iocuni  30473  omsval  30483  omsfval  30484  omsf  30486  oms0  30487  omssubaddlem  30489  omssubadd  30490  carsgval  30493  carsgclctunlem3  30510  omsmeas  30513  elprob  30599  probfinmeasb  30619  probmeasb  30620  dstrvprob  30661  indispconn  31342  iscvm  31367  cvmscld  31381  msrfval  31560  msrval  31561  mthmpps  31605  rdgprc0  31823  rdgprc  31824  dfrdg2  31825  dfrdg3  31826  trpredeq1  31844  trpredeq2  31845  trpredeq3  31846  frecseq123  31902  madeval  32060  unisnif  32157  brapply  32170  isfne  32459  fnemeet2  32487  fnejoin2  32489  tailfval  32492  ordcmp  32571  csbwrecsg  33303  mptsnunlem  33315  dissneqlem  33317  ptrest  33538  mblfinlem2  33577  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  nfunidALT2  34574  nfunidALT  34575  mapdunirnN  37256  aomclem8  37948  dfac21  37953  restuni6  39619  stoweidlem39  40574  salgenuni  40873  caragenval  41028  isome  41029  omeiunle  41052  isomennd  41066  unidmovn  41148  rrnmbl  41149  unidmvon  41152  hspmbl  41164  ovolval4lem2  41185  ovolval5lem2  41188  ovolval5lem3  41189  ovolval5  41190  ovnovollem2  41192  setrecseq  42757
  Copyright terms: Public domain W3C validator