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  27347  oldval  27349  madeoldsuc  27379  unidifsnel  31772  unidifsnne  31773  disjabrex  31813  disjabrexf  31814  fnpreimac  31896  fcnvgreu  31898  xrge0tsmseq  32211  cycpm2tr  32278  qustrivr  32477  ghmquskerlem1  32528  ghmquskerco  32529  gicqusker  32533  lmicqusker  32535  ricqusker  32545  dimval  32686  dimvalfi  32687  algextdeglem1  32772  locfinreflem  32820  locfinref  32821  pstmval  32875  pstmfval  32876  ordtprsuni  32899  esumeq12dvaf  33029  esumeq2  33034  esumval  33044  esumf1o  33048  esumsnf  33062  esumss  33070  esumpfinval  33073  esumpfinvalf  33074  sigapildsys  33160  sxsigon  33190  meascnbl  33217  brae  33239  braew  33240  faeval  33244  imambfm  33261  cnmbfm  33262  dya2iocuni  33282  omsval  33292  omsfval  33293  omsf  33295  oms0  33296  omssubaddlem  33298  omssubadd  33299  carsgval  33302  carsgclctunlem3  33319  omsmeas  33322  elprob  33408  probfinmeasb  33427  probmeasb  33429  dstrvprob  33470  indispconn  34225  iscvm  34250  cvmscld  34264  msrfval  34528  msrval  34529  mthmpps  34573  rdgprc0  34765  rdgprc  34766  dfrdg2  34767  dfrdg3  34768  unisnif  34897  brapply  34910  isfne  35224  fnemeet2  35252  fnejoin2  35254  tailfval  35257  ordcmp  35332  bj-imafv  36132  mptsnunlem  36219  dissneqlem  36221  ctbssinf  36287  ptrest  36487  mblfinlem2  36526  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  nfunidALT2  37839  nfunidALT  37840  mapdunirnN  40521  prjcrvfval  41373  aomclem8  41803  dfac21  41808  rp-unirabeq  41971  rp-tfslim  42103  oaun2  42131  oaun3  42132  ismnu  43020  mnuprdlem1  43031  mnuprdlem2  43032  grumnudlem  43044  grumnud  43045  ismnushort  43060  restuni6  43811  stoweidlem39  44755  salgenuni  45053  caragenval  45209  isome  45210  omeiunle  45233  isomennd  45247  unidmovn  45329  rrnmbl  45330  unidmvon  45333  hspmbl  45345  ovolval4lem2  45366  ovolval5lem2  45369  ovolval5lem3  45370  ovolval5  45371  ovnovollem2  45373  afv2eq12d  45923  uniimaelsetpreimafv  46064  fundcmpsurinjlem3  46068  imasetpreimafvbijlemfo  46073  fundcmpsurbijinjpreimafv  46075  restcls2lem  47545  mreclat  47622  toplatglb  47626  setrecseq  47730