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

Theorem unieqd 4417
 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 4415 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2syl 17 1 (𝜑 𝐴 = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1480  ∪ cuni 4407 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-uni 4408 This theorem is referenced by:  uniprg  4421  unisng  4423  unisn3  4424  csbuni  4437  unisn2  4759  opswap  5586  unixpid  5634  iotaeq  5823  iotabi  5824  uniabio  5825  iotanul  5830  funfv  6227  funfv2  6228  fvun  6230  dffv2  6233  fniunfv  6465  ordunisuc  6986  orduniss2  6987  onsucuni2  6988  elxp4  7064  elxp5  7065  1stval  7122  2ndval  7123  1stnpr  7124  2ndnpr  7125  fo1st  7140  fo2nd  7141  f1stres  7142  f2ndres  7143  1st2val  7146  2nd2val  7147  2nd1st  7165  cnvf1olem  7227  brtpos2  7310  dftpos4  7323  tpostpos  7324  wrecseq123  7360  tz7.44-2  7455  tz7.44-3  7456  rdglim2  7480  ixpsnf1o  7900  xpcomco  8002  xpassen  8006  xpdom2  8007  supeq1  8303  supeq2  8306  supeq3  8307  supeq123d  8308  supval2  8313  rankuni  8678  en2other2  8784  dfac2a  8904  dfac12lem1  8917  dfac12r  8920  kmlem9  8932  kmlem11  8934  kmlem12  8935  enfin2i  9095  fin23lem29  9115  fin23lem30  9116  fin23lem32  9118  fin23lem34  9120  fin23lem35  9121  fin23lem36  9122  fin23lem38  9123  fin23lem39  9124  fin23lem41  9126  isf34lem7  9153  isf34lem6  9154  fin1a2lem10  9183  fin1a2lem11  9184  fin1a2lem12  9185  itunisuc  9193  itunitc  9195  ttukeylem3  9285  ttukey2g  9290  pwcfsdom  9357  gruurn  9572  dfinfre  10956  relexpfld  13731  fsumcnv  14443  fprodcnv  14649  mrcun  16214  isacs1i  16250  mreacs  16251  arwval  16625  ipoval  17086  isacs5lem  17101  acsdrscl  17102  acsficl  17103  isps  17134  isdir  17164  pmtrval  17803  pmtrfv  17804  pmtrprfv  17805  pmtrdifellem3  17830  pmtrprfval  17839  gsumcom2  18306  dmdprd  18329  dprddisj  18340  dprdf1o  18363  dprdsn  18367  dprd2da  18373  dprd2db  18374  dmdprdsplit2lem  18376  lspuni0  18942  lss0v  18948  zrhval  19788  zrhval2  19789  zrhpropd  19795  isbasisg  20675  basis1  20678  baspartn  20682  tgval  20683  eltg  20685  ntrfval  20751  ntrval  20763  tgrest  20886  restuni2  20894  lmfval  20959  cnfval  20960  cnpfval  20961  pnrmopn  21070  fiuncmp  21130  cmpfi  21134  ptval  21296  ptpjpre1  21297  elptr2  21300  ptuni2  21302  ptbasin  21303  ptbasfi  21307  xkoval  21313  txtopon  21317  ptuni  21320  ptunimpt  21321  xkouni  21325  ptpjcn  21337  ptcld  21339  dfac14  21344  ptcnp  21348  prdstopn  21354  ptrescn  21365  txcmplem2  21368  xkoptsub  21380  xkopt  21381  qtopval  21421  qtopeu  21442  hmphindis  21523  txswaphmeolem  21530  ptuncnv  21533  ptunhmeo  21534  xpstopnlem1  21535  flimval  21690  fcfval  21760  alexsubALTlem3  21776  ptcmplem1  21779  ptcmplem2  21780  ptcmplem3  21781  ptcmplem4  21782  ptcmpg  21784  cnextfres1  21795  cldsubg  21837  utopval  21959  tusval  21993  tuslem  21994  tususs  21997  ucnval  22004  prdsxmslem2  22257  ishtpy  22694  pi1buni  22763  pi1xfrcnv  22780  elovolmr  23167  ovoliunlem3  23195  uniioombllem2  23274  uniioombllem3  23276  dyadmbl  23291  vmaval  24756  vmappw  24759  disjabrex  29263  disjabrexf  29264  fcnvgreu  29338  xrge0tsmseq  29596  locfinreflem  29713  locfinref  29714  pstmval  29744  pstmfval  29745  ordtprsuni  29771  esumeq12dvaf  29898  esumeq2  29903  esumval  29913  esumf1o  29917  esumsnf  29931  esumss  29939  esumpfinval  29942  esumpfinvalf  29943  sigapildsys  30030  sxsigon  30060  meascnbl  30087  brae  30109  braew  30110  faeval  30114  imambfm  30129  cnmbfm  30130  dya2iocuni  30150  omsval  30160  omsfval  30161  omsf  30163  oms0  30164  omssubaddlem  30166  omssubadd  30167  carsgval  30170  carsgclctunlem3  30187  omsmeas  30190  elprob  30276  probfinmeasb  30296  probmeasb  30297  dstrvprob  30338  indispconn  30959  iscvm  30984  cvmscld  30998  msrfval  31177  msrval  31178  mthmpps  31222  rdgprc0  31435  rdgprc  31436  dfrdg2  31437  dfrdg3  31438  trpredeq1  31456  trpredeq2  31457  trpredeq3  31458  unisnif  31709  brapply  31722  isfne  32011  fnemeet2  32039  fnejoin2  32041  tailfval  32044  ordcmp  32123  csbwrecsg  32840  mptsnunlem  32852  dissneqlem  32854  ptrest  33075  mblfinlem2  33114  ovoliunnfl  33118  voliunnfl  33120  volsupnfl  33121  nfunidALT2  33771  nfunidALT  33772  mapdunirnN  36454  aomclem8  37146  dfac21  37151  csbfv12gALTOLD  38570  restuni6  38826  stoweidlem39  39589  salgenuni  39888  caragenval  40040  isome  40041  omeiunle  40064  isomennd  40078  unidmovn  40160  rrnmbl  40161  unidmvon  40164  hspmbl  40176  ovolval4lem2  40197  ovolval5lem2  40200  ovolval5lem3  40201  ovolval5  40202  ovnovollem2  40204  setrecseq  41751
 Copyright terms: Public domain W3C validator