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

Theorem unieqd 4814
 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 4811 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2syl 17 1 (𝜑 𝐴 = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538  ∪ cuni 4800 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801 This theorem is referenced by:  uniprg  4818  unisn3  4821  csbuni  4829  unisn2  5180  opswap  6053  unixpid  6103  iotaeq  6295  iotabi  6296  uniabio  6297  iotanul  6302  funfv  6725  funfv2  6726  fvun  6728  dffv2  6733  fniunfv  6984  ordunisuc  7529  orduniss2  7530  onsucuni2  7531  elxp4  7611  elxp5  7612  1stval  7675  2ndval  7676  1stnpr  7677  2ndnpr  7678  fo1st  7693  fo2nd  7694  f1stres  7697  f2ndres  7698  1st2val  7701  2nd2val  7702  2nd1st  7721  cnvf1olem  7790  brtpos2  7883  dftpos4  7896  tpostpos  7897  wrecseq123  7933  tz7.44-2  8028  tz7.44-3  8029  rdglim2  8053  ixpsnf1o  8487  xpcomco  8592  xpassen  8596  xpdom2  8597  supeq1  8895  supeq2  8898  supeq3  8899  supeq123d  8900  supval2  8905  rankuni  9278  en2other2  9422  dfac2a  9542  dfac12lem1  9556  dfac12r  9559  kmlem9  9571  kmlem11  9573  kmlem12  9574  enfin2i  9734  fin23lem29  9754  fin23lem30  9755  fin23lem32  9757  fin23lem34  9759  fin23lem35  9760  fin23lem36  9761  fin23lem38  9762  fin23lem39  9763  fin23lem41  9765  isf34lem7  9792  isf34lem6  9793  fin1a2lem10  9822  fin1a2lem11  9823  fin1a2lem12  9824  itunisuc  9832  itunitc  9834  ttukeylem3  9924  ttukey2g  9929  pwcfsdom  9996  gruurn  10211  dfinfre  11611  relexpfld  14402  relexpfldd  14403  fsumcnv  15122  fprodcnv  15331  mrcun  16887  isacs1i  16922  mreacs  16923  arwval  17297  ipoval  17758  isacs5lem  17773  acsdrscl  17774  acsficl  17775  isps  17806  isdir  17836  pmtrval  18574  pmtrfv  18575  pmtrprfv  18576  pmtrdifellem3  18601  pmtrprfval  18610  gsumcom2  19091  dmdprd  19116  dprddisj  19127  dprdf1o  19150  dprdsn  19154  dprd2da  19160  dprd2db  19161  dmdprdsplit2lem  19163  lspuni0  19778  lss0v  19784  zrhval  20205  zrhval2  20206  zrhpropd  20212  isbasisg  21559  basis1  21562  baspartn  21566  tgval  21567  eltg  21569  ntrfval  21636  ntrval  21648  tgrest  21771  restuni2  21779  lmfval  21844  cnfval  21845  cnpfval  21846  pnrmopn  21955  fiuncmp  22016  cmpfi  22020  ptval  22182  ptpjpre1  22183  elptr2  22186  ptuni2  22188  ptbasin  22189  ptbasfi  22193  xkoval  22199  txtopon  22203  ptuni  22206  ptunimpt  22207  xkouni  22211  ptpjcn  22223  ptcld  22225  dfac14  22230  ptcnp  22234  prdstopn  22240  ptrescn  22251  txcmplem2  22254  xkoptsub  22266  xkopt  22267  qtopval  22307  qtopeu  22328  hmphindis  22409  txswaphmeolem  22416  ptuncnv  22419  ptunhmeo  22420  xpstopnlem1  22421  flimval  22575  fcfval  22645  alexsubALTlem3  22661  ptcmplem1  22664  ptcmplem2  22665  ptcmplem3  22666  ptcmplem4  22667  ptcmpg  22669  cnextfres1  22680  cldsubg  22723  utopval  22845  tusval  22879  tuslem  22880  tususs  22883  ucnval  22890  prdsxmslem2  23143  ishtpy  23584  pi1buni  23652  pi1xfrcnv  23669  elovolmr  24087  ovoliunlem3  24115  uniioombllem2  24194  uniioombllem3  24196  dyadmbl  24211  vmaval  25705  vmappw  25708  unidifsnel  30314  unidifsnne  30315  disjabrex  30352  disjabrexf  30353  fnpreimac  30441  fcnvgreu  30443  xrge0tsmseq  30751  cycpm2tr  30818  qustrivr  30988  dimval  31101  dimvalfi  31102  locfinreflem  31205  locfinref  31206  pstmval  31260  pstmfval  31261  ordtprsuni  31284  esumeq12dvaf  31412  esumeq2  31417  esumval  31427  esumf1o  31431  esumsnf  31445  esumss  31453  esumpfinval  31456  esumpfinvalf  31457  sigapildsys  31543  sxsigon  31573  meascnbl  31600  brae  31622  braew  31623  faeval  31627  imambfm  31642  cnmbfm  31643  dya2iocuni  31663  omsval  31673  omsfval  31674  omsf  31676  oms0  31677  omssubaddlem  31679  omssubadd  31680  carsgval  31683  carsgclctunlem3  31700  omsmeas  31703  elprob  31789  probfinmeasb  31808  probmeasb  31810  dstrvprob  31851  indispconn  32606  iscvm  32631  cvmscld  32645  msrfval  32909  msrval  32910  mthmpps  32954  rdgprc0  33163  rdgprc  33164  dfrdg2  33165  dfrdg3  33166  trpredeq1  33184  trpredeq2  33185  trpredeq3  33186  frecseq123  33244  madeval  33414  unisnif  33511  brapply  33524  isfne  33812  fnemeet2  33840  fnejoin2  33842  tailfval  33845  ordcmp  33920  bj-imafv  34682  csbwrecsg  34760  mptsnunlem  34771  dissneqlem  34773  ctbssinf  34839  ptrest  35072  mblfinlem2  35111  ovoliunnfl  35115  voliunnfl  35117  volsupnfl  35118  nfunidALT2  36281  nfunidALT  36282  mapdunirnN  38962  aomclem8  40020  dfac21  40025  ismnu  40984  mnuprdlem1  40995  mnuprdlem2  40996  grumnudlem  41008  grumnud  41009  restuni6  41772  stoweidlem39  42696  salgenuni  42992  caragenval  43147  isome  43148  omeiunle  43171  isomennd  43185  unidmovn  43267  rrnmbl  43268  unidmvon  43271  hspmbl  43283  ovolval4lem2  43304  ovolval5lem2  43307  ovolval5lem3  43308  ovolval5  43309  ovnovollem2  43311  afv2eq12d  43786  uniimaelsetpreimafv  43928  fundcmpsurinjlem3  43932  imasetpreimafvbijlemfo  43937  fundcmpsurbijinjpreimafv  43939  setrecseq  45229
 Copyright terms: Public domain W3C validator