Theorem unieqd 4924

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 4922	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵)

Syntax hints:   → wi 4   = wceq 1536  ∪ cuni 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-uni 4912

This theorem is referenced by:  unisn3  4932  csbuni  4940  unisn2  5317  opswap  6250  unixpid  6305  iotaeq  6527  iotabi  6528  uniabio  6529  iotanul  6540  funfv  6995  funfv2  6996  fvun  6998  dffv2  7003  fniunfv  7266  ordunisuc  7851  orduniss2  7852  onsucuni2  7853  elxp4  7944  elxp5  7945  1stval  8014  2ndval  8015  1stnpr  8016  2ndnpr  8017  fo1st  8032  fo2nd  8033  f1stres  8036  f2ndres  8037  1st2val  8040  2nd2val  8041  2nd1st  8061  cnvf1olem  8133  brtpos2  8255  dftpos4  8268  tpostpos  8269  frecseq123  8305  csbfrecsg  8307  wrecseq123OLD  8338  tz7.44-2  8445  tz7.44-3  8446  rdglim2  8470  ixpsnf1o  8976  xpcomco  9100  xpassen  9104  xpdom2  9105  supeq1  9482  supeq2  9485  supeq3  9486  supeq123d  9487  supval2  9492  rankuni  9900  en2other2  10046  dfac2a  10167  dfac12lem1  10181  dfac12r  10184  kmlem9  10196  kmlem11  10198  kmlem12  10199  enfin2i  10358  fin23lem29  10378  fin23lem30  10379  fin23lem32  10381  fin23lem34  10383  fin23lem35  10384  fin23lem36  10385  fin23lem38  10386  fin23lem39  10387  fin23lem41  10389  isf34lem7  10416  isf34lem6  10417  fin1a2lem10  10446  fin1a2lem11  10447  fin1a2lem12  10448  itunisuc  10456  itunitc  10458  ttukeylem3  10548  ttukey2g  10553  pwcfsdom  10620  gruurn  10835  dfinfre  12246  relexpfld  15084  relexpfldd  15085  fsumcnv  15805  fprodcnv  16015  mrcun  17666  isacs1i  17701  mreacs  17702  arwval  18096  ipoval  18587  isacs5lem  18602  acsdrscl  18603  acsficl  18604  isps  18625  isdir  18655  ghmqusnsglem1  19310  ghmquskerlem1  19313  ghmquskerco  19314  gicqusker  19318  pmtrval  19483  pmtrfv  19484  pmtrprfv  19485  pmtrdifellem3  19510  pmtrprfval  19519  gsumcom2  20007  dmdprd  20032  dprddisj  20043  dprdf1o  20066  dprdsn  20070  dprd2da  20076  dprd2db  20077  dmdprdsplit2lem  20079  lspuni0  21025  lss0v  21032  zrhval  21535  zrhval2  21536  zrhpropd  21542  isbasisg  22969  basis1  22972  baspartn  22976  tgval  22977  eltg  22979  ntrfval  23047  ntrval  23059  tgrest  23182  restuni2  23190  lmfval  23255  cnfval  23256  cnpfval  23257  pnrmopn  23366  fiuncmp  23427  cmpfi  23431  ptval  23593  ptpjpre1  23594  elptr2  23597  ptuni2  23599  ptbasin  23600  ptbasfi  23604  xkoval  23610  txtopon  23614  ptuni  23617  ptunimpt  23618  xkouni  23622  ptpjcn  23634  ptcld  23636  dfac14  23641  ptcnp  23645  prdstopn  23651  ptrescn  23662  txcmplem2  23665  xkoptsub  23677  xkopt  23678  qtopval  23718  qtopeu  23739  hmphindis  23820  txswaphmeolem  23827  ptuncnv  23830  ptunhmeo  23831  xpstopnlem1  23832  flimval  23986  fcfval  24056  alexsubALTlem3  24072  ptcmplem1  24075  ptcmplem2  24076  ptcmplem3  24077  ptcmplem4  24078  ptcmpg  24080  cnextfres1  24091  cldsubg  24134  utopval  24256  tusval  24289  tuslem  24290  tuslemOLD  24291  tususs  24294  ucnval  24301  prdsxmslem2  24557  ishtpy  25017  pi1buni  25086  pi1xfrcnv  25103  elovolmr  25524  ovoliunlem3  25552  uniioombllem2  25631  uniioombllem3  25633  dyadmbl  25648  vmaval  27170  vmappw  27173  madeval  27905  oldval  27907  madeoldsuc  27937  zs12bday  28438  unidifsnel  32560  unidifsnne  32561  disjabrex  32601  disjabrexf  32602  fnpreimac  32687  fcnvgreu  32689  xrge0tsmseq  33049  cycpm2tr  33121  qustrivr  33372  lmicqusker  33425  ricqusker  33434  dimval  33627  dimvalfi  33628  algextdeglem4  33725  algextdeg  33730  locfinreflem  33800  locfinref  33801  pstmval  33855  pstmfval  33856  ordtprsuni  33879  esumeq12dvaf  34011  esumeq2  34016  esumval  34026  esumf1o  34030  esumsnf  34044  esumss  34052  esumpfinval  34055  esumpfinvalf  34056  sigapildsys  34142  sxsigon  34172  meascnbl  34199  brae  34221  braew  34222  faeval  34226  imambfm  34243  cnmbfm  34244  dya2iocuni  34264  omsval  34274  omsfval  34275  omsf  34277  oms0  34278  omssubaddlem  34280  omssubadd  34281  carsgval  34284  carsgclctunlem3  34301  omsmeas  34304  elprob  34390  probfinmeasb  34409  probmeasb  34411  dstrvprob  34452  wevgblacfn  35092  indispconn  35218  iscvm  35243  cvmscld  35257  msrfval  35521  msrval  35522  mthmpps  35566  rdgprc0  35774  rdgprc  35775  dfrdg2  35776  dfrdg3  35777  unisnif  35906  brapply  35919  cbviotadavw  36251  isfne  36321  fnemeet2  36349  fnejoin2  36351  tailfval  36354  ordcmp  36429  bj-imafv  37233  mptsnunlem  37320  dissneqlem  37322  ctbssinf  37388  ptrest  37605  mblfinlem2  37644  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  nfunidALT2  38950  nfunidALT  38951  mapdunirnN  41632  zndvdchrrhm  41952  aks6d1c7lem2  42162  aks5lem4a  42171  prjcrvfval  42617  aomclem8  43049  dfac21  43054  rp-unirabeq  43210  rp-tfslim  43342  oaun2  43370  oaun3  43371  ismnu  44256  mnuprdlem1  44267  mnuprdlem2  44268  grumnudlem  44280  grumnud  44281  ismnushort  44296  restuni6  45061  stoweidlem39  45994  salgenuni  46292  caragenval  46448  isome  46449  omeiunle  46472  isomennd  46486  unidmovn  46568  rrnmbl  46569  unidmvon  46572  hspmbl  46584  ovolval4lem2  46605  ovolval5lem2  46608  ovolval5lem3  46609  ovolval5  46610  ovnovollem2  46612  afv2eq12d  47164  uniimaelsetpreimafv  47320  fundcmpsurinjlem3  47324  imasetpreimafvbijlemfo  47329  fundcmpsurbijinjpreimafv  47331  restcls2lem  48708  mreclat  48785  toplatglb  48789  setrecseq  48915