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

Theorem unieqd 4232
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 4230 . 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 1437   U.cuni 4222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788  df-uni 4223
This theorem is referenced by:  uniprg  4236  unisng  4238  unisn3  4239  csbuni  4250  unisn2  4561  opswap  5343  unixpid  5391  iotaeq  5573  iotabi  5574  uniabio  5575  iotanul  5580  funfv  5948  funfv2  5949  fvun  5951  dffv2  5954  fniunfv  6167  ordunisuc  6673  orduniss2  6674  onsucuni2  6675  elxp4  6751  elxp5  6752  1stval  6809  2ndval  6810  1stnpr  6811  2ndnpr  6812  fo1st  6827  fo2nd  6828  f1stres  6829  f2ndres  6830  1st2val  6833  2nd2val  6834  2nd1st  6852  cnvf1olem  6905  brtpos2  6987  dftpos4  7000  tpostpos  7001  wrecseq123  7037  tz7.44-2  7133  tz7.44-3  7134  rdglim2  7158  ixpsnf1o  7570  xpcomco  7668  xpassen  7672  xpdom2  7673  supeq1  7965  supeq2  7968  supeq3  7969  supeq123d  7970  supval2  7975  rankuni  8333  en2other2  8439  dfac2a  8558  dfac12lem1  8571  dfac12r  8574  kmlem9  8586  kmlem11  8588  kmlem12  8589  enfin2i  8749  fin23lem29  8769  fin23lem30  8770  fin23lem32  8772  fin23lem34  8774  fin23lem35  8775  fin23lem36  8776  fin23lem38  8777  fin23lem39  8778  fin23lem41  8780  isf34lem7  8807  isf34lem6  8808  fin1a2lem10  8837  fin1a2lem11  8838  fin1a2lem12  8839  itunisuc  8847  itunitc  8849  ttukeylem3  8939  ttukey2g  8944  pwcfsdom  9006  gruurn  9222  dfinfre  10588  dfinfmrOLD  10589  relexpfld  13091  fsumcnv  13812  fprodcnv  14015  mrcun  15479  isacs1i  15514  mreacs  15515  arwval  15889  ipoval  16351  isacs5lem  16366  acsdrscl  16367  acsficl  16368  isps  16399  isdir  16429  pmtrval  17043  pmtrfv  17044  pmtrprfv  17045  pmtrdifellem3  17070  pmtrprfval  17079  gsumcom2  17542  dmdprd  17565  dprddisj  17576  dprdf1o  17600  dprdsn  17604  dprd2da  17610  dprd2db  17611  dmdprdsplit2lem  17613  lspuni0  18168  lss0v  18174  zrhval  19010  zrhval2  19011  zrhpropd  19017  isbasisg  19893  basis1  19896  baspartn  19900  tgval  19901  eltg  19903  ntrfval  19970  ntrval  19982  tgrest  20106  restuni2  20114  lmfval  20179  cnfval  20180  cnpfval  20181  pnrmopn  20290  fiuncmp  20350  cmpfi  20354  ptval  20516  ptpjpre1  20517  elptr2  20520  ptuni2  20522  ptbasin  20523  ptbasfi  20527  xkoval  20533  txtopon  20537  ptuni  20540  ptunimpt  20541  xkouni  20545  ptpjcn  20557  ptcld  20559  dfac14  20564  ptcnp  20568  prdstopn  20574  ptrescn  20585  txcmplem2  20588  xkoptsub  20600  xkopt  20601  qtopval  20641  qtopeu  20662  hmphindis  20743  txswaphmeolem  20750  ptuncnv  20753  ptunhmeo  20754  xpstopnlem1  20755  flimval  20909  fcfval  20979  alexsubALTlem3  20995  ptcmplem1  20998  ptcmplem2  20999  ptcmplem3  21000  ptcmplem4  21001  ptcmpg  21003  cnextfres1  21014  cldsubg  21056  utopval  21178  tusval  21212  tuslem  21213  tususs  21216  ucnval  21223  prdsxmslem2  21475  ishtpy  21896  pi1buni  21964  pi1xfrcnv  21981  elovolmr  22307  ovoliunlem3  22335  uniioombllem2  22417  uniioombllem2OLD  22418  uniioombllem3  22420  dyadmbl  22435  vmaval  23903  vmappw  23906  disjabrex  28031  disjabrexf  28032  fcnvgreu  28115  xrge0tsmseq  28389  locfinreflem  28506  locfinref  28507  pstmval  28537  pstmfval  28538  ordtprsuni  28564  esumeq12dvaf  28691  esumeq2  28696  esumval  28706  esumf1o  28710  esumsnf  28724  esumss  28732  esumpfinval  28735  esumpfinvalf  28736  sigapildsys  28823  sxsigon  28853  meascnbl  28880  brae  28903  braew  28904  faeval  28908  imambfm  28923  cnmbfm  28924  dya2iocuni  28944  omsval  28954  omsfval  28955  omsf  28957  oms0  28958  omssubaddlem  28960  omssubadd  28961  carsgval  28964  carsgclctunlem3  28981  omsmeas  28984  elprob  29068  probfinmeasb  29088  probmeasb  29089  dstrvprob  29130  indispcon  29745  iscvm  29770  cvmscld  29784  msrfval  29963  msrval  29964  mthmpps  30008  rdgprc0  30227  rdgprc  30228  dfrdg2  30229  dfrdg3  30230  trpredeq1  30248  trpredeq2  30249  trpredeq3  30250  nofulllem1  30376  nofulllem2  30377  unisnif  30477  brapply  30490  isfne  30780  fnemeet2  30808  fnejoin2  30810  tailfval  30813  ordcmp  30892  mptsnunlem  31474  dissneqlem  31476  ptrest  31642  mblfinlem2  31681  ovoliunnfl  31685  voliunnfl  31687  volsupnfl  31688  mapdunirnN  34926  aomclem8  35624  dfac21  35629  csbfv12gALTOLD  36852  stoweidlem39  37468  caragenval  37822  isome  37823  omeiunle  37846
  Copyright terms: Public domain W3C validator