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

Theorem unieqd 3838
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 3836 . 2  |-  ( A  =  B  ->  U. A  =  U. B )
31, 2syl 15 1  |-  ( ph  ->  U. A  =  U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   U.cuni 3827
This theorem is referenced by:  uniprg  3842  unisng  3844  unisn2  4522  unisn3  4523  ordunisuc  4623  orduniss2  4624  onsucuni2  4625  opswap  5159  elxp4  5160  elxp5  5161  unixpid  5207  iotaeq  5227  iotabi  5228  uniabio  5229  iotanul  5234  csbfv12gALT  5536  funfv  5586  funfv2  5587  fvun  5589  dffv2  5592  fniunfv  5773  1stval  6124  2ndval  6125  fo1st  6139  fo2nd  6140  f1stres  6141  f2ndres  6142  1st2val  6145  2nd2val  6146  2nd1st  6165  cnvf1olem  6216  brtpos2  6240  dftpos4  6253  tpostpos  6254  recseq  6389  tz7.44-2  6420  tz7.44-3  6421  rdglim2  6445  ixpsnf1o  6856  xpcomco  6952  xpassen  6956  xpdom2  6957  supeq1  7198  supeq2  7201  rankuni  7535  dfac2a  7756  dfac12lem1  7769  dfac12r  7772  kmlem9  7784  kmlem11  7786  kmlem12  7787  enfin2i  7947  fin23lem29  7967  fin23lem30  7968  fin23lem32  7970  fin23lem34  7972  fin23lem35  7973  fin23lem36  7974  fin23lem38  7975  fin23lem39  7976  fin23lem41  7978  isf34lem7  8005  isf34lem6  8006  fin1a2lem10  8035  fin1a2lem11  8036  fin1a2lem12  8037  itunisuc  8045  itunitc  8047  ttukeylem3  8138  ttukey2g  8143  pwcfsdom  8205  gruurn  8420  dfinfmr  9731  fsumcnv  12236  xpnnenOLD  12488  mrcun  13524  isacs1i  13559  mreacs  13560  arwval  13875  ipoval  14257  isacs5lem  14272  acsdrscl  14273  acsficl  14274  isps  14311  spwval2  14333  isdir  14354  gsumcom2  15226  dmdprd  15236  dprddisj  15244  dprdf1o  15267  dprdsn  15271  dprd2da  15277  dprd2db  15278  dmdprdsplit2lem  15280  lspuni0  15767  lss0v  15773  zrhval  16462  zrhval2  16463  zrhpropd  16469  isbasisg  16685  basis1  16688  baspartn  16692  tgval  16693  eltg  16695  ntrfval  16761  ntrval  16773  tgrest  16890  restuni2  16898  lmfval  16962  cnfval  16963  cnpfval  16964  pnrmopn  17071  fiuncmp  17131  cmpfi  17135  ptval  17265  ptpjpre1  17266  elptr2  17269  ptuni2  17271  ptbasin  17272  ptbasfi  17276  xkoval  17282  txtopon  17286  ptuni  17289  ptunimpt  17290  xkouni  17294  ptpjcn  17305  ptcld  17307  dfac14  17312  ptcnp  17316  prdstopn  17322  ptrescn  17333  txcmplem2  17336  xkoptsub  17348  xkopt  17349  qtopval  17386  qtopeu  17407  hmphindis  17488  txswaphmeolem  17495  ptuncnv  17498  ptunhmeo  17499  xpstopnlem1  17500  flimval  17658  fcfval  17728  alexsubALTlem3  17743  ptcmplem1  17746  ptcmplem2  17747  ptcmplem3  17748  ptcmplem4  17749  ptcmpg  17751  cldsubg  17793  prdsxmslem2  18075  ishtpy  18470  pi1buni  18538  pi1xfrcnv  18555  elovolmr  18835  ovoliunlem3  18863  uniioombllem2  18938  uniioombllem3  18940  dyadmbl  18955  vmaval  20351  vmappw  20354  1stnpr  23245  2ndnpr  23246  disjabrex  23359  disjabrexf  23360  xrge0tsmseq  23384  esumeq12dvaf  23414  esumeq2  23418  esumval  23425  esumf1o  23429  esumsn  23437  esumss  23440  esumpfinval  23443  esumpfinvalf  23444  sxsigon  23523  meascnbl  23546  imambfm  23567  cnmbfm  23568  isibfm  23593  elprob  23612  probfinmeasb  23632  probmeasb  23633  dstrvprob  23672  indispcon  23765  iscvm  23790  cvmscld  23804  relexp0  24025  relexpsucr  24026  rdgprc0  24150  rdgprc  24151  dfrdg2  24152  dfrdg3  24153  trpredeq1  24223  trpredeq2  24224  trpredeq3  24225  nofulllem1  24356  nofulllem2  24357  unisnif  24464  brapply  24477  funpartfv  24483  bpolylem  24783  ordcmp  24886  isprsr  25224  ubos  25256  mxlelt  25264  mnlelt2  25266  isdir2  25292  usptoplem  25546  istopx  25547  istopxc  25548  usptop  25550  prcnt  25551  unexun  25569  supexr  25631  vtarl  25887  isfne  26268  fnemeet2  26316  fnejoin2  26318  tailfval  26321  supeq123d  27158  aomclem8  27159  dfac21  27164  en2other2  27382  pmtrval  27394  pmtrfv  27395  pmtrprfv  27396  stoweidlem39  27788  mapdunirnN  31840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-uni 3828
  Copyright terms: Public domain W3C validator