Theorem unieqd 4854

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

Syntax hints:   → wi 4   = wceq 1548  ∪ cuni 4841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-uni 4842

This theorem is referenced by:  unisn3  4862  csbuni  4871  unisn2  5237  opswap  6184  unixpid  6239  iotaeq  6457  iotabi  6458  uniabio  6459  iotanul  6469  funfv  6918  funfv2  6919  fvun  6921  dffv2  6926  fniunfv  7195  ordunisuc  7776  orduniss2  7777  onsucuni2  7778  elxp4  7866  elxp5  7867  1stval  7937  2ndval  7938  1stnpr  7939  2ndnpr  7940  fo1st  7955  fo2nd  7956  f1stres  7959  f2ndres  7960  1st2val  7963  2nd2val  7964  2nd1st  7984  cnvf1olem  8053  brtpos2  8176  dftpos4  8189  tpostpos  8190  frecseq123  8226  csbfrecsg  8228  tz7.44-2  8340  tz7.44-3  8341  rdglim2  8365  ixpsnf1o  8880  xpcomco  8999  xpassen  9003  xpdom2  9004  supeq1  9352  supeq2  9355  supeq3  9356  supeq123d  9357  supval2  9362  rankuni  9782  en2other2  9926  dfac2a  10047  dfac12lem1  10061  dfac12r  10064  kmlem9  10076  kmlem11  10078  kmlem12  10079  enfin2i  10238  fin23lem29  10258  fin23lem30  10259  fin23lem32  10261  fin23lem34  10263  fin23lem35  10264  fin23lem36  10265  fin23lem38  10266  fin23lem39  10267  fin23lem41  10269  isf34lem7  10296  isf34lem6  10297  fin1a2lem10  10326  fin1a2lem11  10327  fin1a2lem12  10328  itunisuc  10336  itunitc  10338  ttukeylem3  10428  ttukey2g  10433  pwcfsdom  10501  gruurn  10716  dfinfre  12132  relexpfld  15006  relexpfldd  15007  fsumcnv  15730  fprodcnv  15943  mrcun  17583  isacs1i  17618  mreacs  17619  arwval  18005  ipoval  18491  isacs5lem  18506  acsdrscl  18507  acsficl  18508  isps  18529  isdir  18559  ghmqusnsglem1  19250  ghmquskerlem1  19253  ghmquskerco  19254  gicqusker  19258  pmtrval  19421  pmtrfv  19422  pmtrprfv  19423  pmtrdifellem3  19448  pmtrprfval  19457  gsumcom2  19945  dmdprd  19970  dprddisj  19981  dprdf1o  20004  dprdsn  20008  dprd2da  20014  dprd2db  20015  dmdprdsplit2lem  20017  lspuni0  21004  lss0v  21010  zrhval  21486  zrhval2  21487  zrhpropd  21493  isbasisg  22934  basis1  22937  baspartn  22941  tgval  22942  eltg  22944  ntrfval  23011  ntrval  23023  tgrest  23146  restuni2  23154  lmfval  23219  cnfval  23220  cnpfval  23221  pnrmopn  23330  fiuncmp  23391  cmpfi  23395  ptval  23557  ptpjpre1  23558  elptr2  23561  ptuni2  23563  ptbasin  23564  ptbasfi  23568  xkoval  23574  txtopon  23578  ptuni  23581  ptunimpt  23582  xkouni  23586  ptpjcn  23598  ptcld  23600  dfac14  23605  ptcnp  23609  prdstopn  23615  ptrescn  23626  txcmplem2  23629  xkoptsub  23641  xkopt  23642  qtopval  23682  qtopeu  23703  hmphindis  23784  txswaphmeolem  23791  ptuncnv  23794  ptunhmeo  23795  xpstopnlem1  23796  flimval  23950  fcfval  24020  alexsubALTlem3  24036  ptcmplem1  24039  ptcmplem2  24040  ptcmplem3  24041  ptcmplem4  24042  ptcmpg  24044  cnextfres1  24055  cldsubg  24098  utopval  24219  tusval  24252  tuslem  24253  tususs  24256  ucnval  24263  prdsxmslem2  24516  ishtpy  24961  pi1buni  25029  pi1xfrcnv  25046  elovolmr  25465  ovoliunlem3  25493  uniioombllem2  25572  uniioombllem3  25574  dyadmbl  25589  vmaval  27098  vmappw  27101  madeval  27846  oldval  27848  madeoldsuc  27899  unidifsnel  32627  unidifsnne  32628  disjabrex  32675  disjabrexf  32676  fnpreimac  32766  fcnvgreu  32768  xrge0tsmseq  33160  cycpm2tr  33204  qustrivr  33452  lmicqusker  33505  ricqusker  33514  esplyfval1  33769  dimval  33797  dimvalfi  33798  algextdeglem4  33916  algextdeg  33921  locfinreflem  34036  locfinref  34037  pstmval  34091  pstmfval  34092  ordtprsuni  34115  esumeq12dvaf  34227  esumeq2  34232  esumval  34242  esumf1o  34246  esumsnf  34260  esumss  34268  esumpfinval  34271  esumpfinvalf  34272  sigapildsys  34358  sxsigon  34388  meascnbl  34415  brae  34437  braew  34438  faeval  34442  imambfm  34458  cnmbfm  34459  dya2iocuni  34479  omsval  34489  omsfval  34490  omsf  34492  oms0  34493  omssubaddlem  34495  omssubadd  34496  carsgval  34499  carsgclctunlem3  34516  omsmeas  34519  elprob  34605  probfinmeasb  34624  probmeasb  34626  dstrvprob  34668  fineqvnttrclselem1  35317  fineqvnttrclselem2  35318  fineqvnttrclselem3  35319  fineqvnttrclse  35320  fineqvr1ombregs  35334  wevgblacfn  35352  indispconn  35477  iscvm  35502  cvmscld  35516  msrfval  35780  msrval  35781  mthmpps  35825  rdgprc0  36034  rdgprc  36035  dfrdg2  36036  dfrdg3  36037  unisnif  36166  brapply  36179  cbviotadavw  36512  isfne  36582  fnemeet2  36610  fnejoin2  36612  tailfval  36615  ordcmp  36690  ttcid  36735  bj-imafv  37626  mptsnunlem  37715  dissneqlem  37717  ctbssinf  37783  ptrest  38001  mblfinlem2  38040  ovoliunnfl  38044  voliunnfl  38046  volsupnfl  38047  nfunidALT2  39476  nfunidALT  39477  mapdunirnN  42157  zndvdchrrhm  42473  aks6d1c7lem2  42681  aks5lem4a  42690  prjcrvfval  43096  aomclem8  43521  dfac21  43526  rp-unirabeq  43682  rp-tfslim  43813  oaun2  43841  oaun3  43842  ismnu  44720  mnuprdlem1  44731  mnuprdlem2  44732  grumnudlem  44744  grumnud  44745  ismnushort  44760  restuni6  45583  stoweidlem39  46496  salgenuni  46794  caragenval  46950  isome  46951  omeiunle  46974  isomennd  46988  unidmovn  47070  rrnmbl  47071  unidmvon  47074  hspmbl  47086  ovolval4lem2  47107  ovolval5lem2  47110  ovolval5lem3  47111  ovolval5  47112  ovnovollem2  47114  afv2eq12d  47692  uniimaelsetpreimafv  47885  fundcmpsurinjlem3  47889  imasetpreimafvbijlemfo  47894  fundcmpsurbijinjpreimafv  47896  dftpos5  49378  tposideq  49392  restcls2lem  49417  mreclat  49501  toplatglb  49505  swapf1a  49773  swapf2a  49775  swapf1  49776  swapf2  49778  setrecseq  50189