Theorem unieqd 4923

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

Step	Hyp	Ref	Expression
1		unieqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		unieq 4920	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1542  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910

This theorem is referenced by:  uniprgOLD  4929  unisn3  4933  csbuni  4941  unisn2  5313  opswap  6229  unixpid  6284  iotaeq  6509  iotabi  6510  uniabio  6511  iotanul  6522  funfv  6979  funfv2  6980  fvun  6982  dffv2  6987  fniunfv  7246  ordunisuc  7820  orduniss2  7821  onsucuni2  7822  elxp4  7913  elxp5  7914  1stval  7977  2ndval  7978  1stnpr  7979  2ndnpr  7980  fo1st  7995  fo2nd  7996  f1stres  7999  f2ndres  8000  1st2val  8003  2nd2val  8004  2nd1st  8024  cnvf1olem  8096  brtpos2  8217  dftpos4  8230  tpostpos  8231  frecseq123  8267  csbfrecsg  8269  wrecseq123OLD  8300  tz7.44-2  8407  tz7.44-3  8408  rdglim2  8432  ixpsnf1o  8932  xpcomco  9062  xpassen  9066  xpdom2  9067  supeq1  9440  supeq2  9443  supeq3  9444  supeq123d  9445  supval2  9450  rankuni  9858  en2other2  10004  dfac2a  10124  dfac12lem1  10138  dfac12r  10141  kmlem9  10153  kmlem11  10155  kmlem12  10156  enfin2i  10316  fin23lem29  10336  fin23lem30  10337  fin23lem32  10339  fin23lem34  10341  fin23lem35  10342  fin23lem36  10343  fin23lem38  10344  fin23lem39  10345  fin23lem41  10347  isf34lem7  10374  isf34lem6  10375  fin1a2lem10  10404  fin1a2lem11  10405  fin1a2lem12  10406  itunisuc  10414  itunitc  10416  ttukeylem3  10506  ttukey2g  10511  pwcfsdom  10578  gruurn  10793  dfinfre  12195  relexpfld  14996  relexpfldd  14997  fsumcnv  15719  fprodcnv  15927  mrcun  17566  isacs1i  17601  mreacs  17602  arwval  17993  ipoval  18483  isacs5lem  18498  acsdrscl  18499  acsficl  18500  isps  18521  isdir  18551  pmtrval  19319  pmtrfv  19320  pmtrprfv  19321  pmtrdifellem3  19346  pmtrprfval  19355  gsumcom2  19843  dmdprd  19868  dprddisj  19879  dprdf1o  19902  dprdsn  19906  dprd2da  19912  dprd2db  19913  dmdprdsplit2lem  19915  lspuni0  20621  lss0v  20627  zrhval  21057  zrhval2  21058  zrhpropd  21064  isbasisg  22450  basis1  22453  baspartn  22457  tgval  22458  eltg  22460  ntrfval  22528  ntrval  22540  tgrest  22663  restuni2  22671  lmfval  22736  cnfval  22737  cnpfval  22738  pnrmopn  22847  fiuncmp  22908  cmpfi  22912  ptval  23074  ptpjpre1  23075  elptr2  23078  ptuni2  23080  ptbasin  23081  ptbasfi  23085  xkoval  23091  txtopon  23095  ptuni  23098  ptunimpt  23099  xkouni  23103  ptpjcn  23115  ptcld  23117  dfac14  23122  ptcnp  23126  prdstopn  23132  ptrescn  23143  txcmplem2  23146  xkoptsub  23158  xkopt  23159  qtopval  23199  qtopeu  23220  hmphindis  23301  txswaphmeolem  23308  ptuncnv  23311  ptunhmeo  23312  xpstopnlem1  23313  flimval  23467  fcfval  23537  alexsubALTlem3  23553  ptcmplem1  23556  ptcmplem2  23557  ptcmplem3  23558  ptcmplem4  23559  ptcmpg  23561  cnextfres1  23572  cldsubg  23615  utopval  23737  tusval  23770  tuslem  23771  tuslemOLD  23772  tususs  23775  ucnval  23782  prdsxmslem2  24038  ishtpy  24488  pi1buni  24556  pi1xfrcnv  24573  elovolmr  24993  ovoliunlem3  25021  uniioombllem2  25100  uniioombllem3  25102  dyadmbl  25117  vmaval  26617  vmappw  26620  madeval  27348  oldval  27350  madeoldsuc  27380  unidifsnel  31803  unidifsnne  31804  disjabrex  31844  disjabrexf  31845  fnpreimac  31927  fcnvgreu  31929  xrge0tsmseq  32242  cycpm2tr  32309  qustrivr  32508  ghmquskerlem1  32559  ghmquskerco  32560  gicqusker  32564  lmicqusker  32566  ricqusker  32576  dimval  32717  dimvalfi  32718  algextdeglem1  32803  locfinreflem  32851  locfinref  32852  pstmval  32906  pstmfval  32907  ordtprsuni  32930  esumeq12dvaf  33060  esumeq2  33065  esumval  33075  esumf1o  33079  esumsnf  33093  esumss  33101  esumpfinval  33104  esumpfinvalf  33105  sigapildsys  33191  sxsigon  33221  meascnbl  33248  brae  33270  braew  33271  faeval  33275  imambfm  33292  cnmbfm  33293  dya2iocuni  33313  omsval  33323  omsfval  33324  omsf  33326  oms0  33327  omssubaddlem  33329  omssubadd  33330  carsgval  33333  carsgclctunlem3  33350  omsmeas  33353  elprob  33439  probfinmeasb  33458  probmeasb  33460  dstrvprob  33501  indispconn  34256  iscvm  34281  cvmscld  34295  msrfval  34559  msrval  34560  mthmpps  34604  rdgprc0  34796  rdgprc  34797  dfrdg2  34798  dfrdg3  34799  unisnif  34928  brapply  34941  isfne  35272  fnemeet2  35300  fnejoin2  35302  tailfval  35305  ordcmp  35380  bj-imafv  36180  mptsnunlem  36267  dissneqlem  36269  ctbssinf  36335  ptrest  36535  mblfinlem2  36574  ovoliunnfl  36578  voliunnfl  36580  volsupnfl  36581  nfunidALT2  37887  nfunidALT  37888  mapdunirnN  40569  prjcrvfval  41421  aomclem8  41851  dfac21  41856  rp-unirabeq  42019  rp-tfslim  42151  oaun2  42179  oaun3  42180  ismnu  43068  mnuprdlem1  43079  mnuprdlem2  43080  grumnudlem  43092  grumnud  43093  ismnushort  43108  restuni6  43859  stoweidlem39  44803  salgenuni  45101  caragenval  45257  isome  45258  omeiunle  45281  isomennd  45295  unidmovn  45377  rrnmbl  45378  unidmvon  45381  hspmbl  45393  ovolval4lem2  45414  ovolval5lem2  45417  ovolval5lem3  45418  ovolval5  45419  ovnovollem2  45421  afv2eq12d  45971  uniimaelsetpreimafv  46112  fundcmpsurinjlem3  46116  imasetpreimafvbijlemfo  46121  fundcmpsurbijinjpreimafv  46123  restcls2lem  47593  mreclat  47670  toplatglb  47674  setrecseq  47778