Theorem unieqd 4879

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867

This theorem is used by:  unisn3  4887  csbuni  4897  unisn2  5265  opswap  6230  unixpid  6287  iotaeq  6506  iotabi  6507  uniabio  6508  iotanul  6518  funfv  6972  funfv2  6973  fvun  6975  dffv2  6980  fniunfv  7251  ordunisuc  7843  orduniss2  7844  onsucuni2  7845  elxp4  7934  elxp5  7935  1stval  8003  2ndval  8004  1stnpr  8005  2ndnpr  8006  fo1st  8021  fo2nd  8022  f1stres  8025  f2ndres  8026  1st2val  8029  2nd2val  8030  2nd1st  8049  cnvf1olem  8121  brtpos2  8249  dftpos4  8262  tpostpos  8263  frecseq123  8300  csbfrecsg  8302  tz7.44-2  8415  tz7.44-3  8416  rdglim2  8440  ixpsnf1o  8966  xpcomco  9086  xpassen  9090  xpdom2  9091  supeq1  9437  supeq2  9440  supeq3  9441  supeq123d  9442  supval2  9447  rankuni  9879  en2other2  10088  dfac2a  10208  dfac12lem1  10222  dfac12r  10225  kmlem9  10237  kmlem11  10239  kmlem12  10240  enfin2i  10399  fin23lem29  10419  fin23lem30  10420  fin23lem32  10422  fin23lem34  10424  fin23lem35  10425  fin23lem36  10426  fin23lem38  10427  fin23lem39  10428  fin23lem41  10430  isf34lem7  10457  isf34lem6  10458  fin1a2lem10  10487  fin1a2lem11  10488  fin1a2lem12  10489  itunisuc  10497  itunitc  10499  ttukeylem3  10589  ttukey2g  10594  pwcfsdom  10668  gruurn  10883  dfinfre  12298  relexpfld  15202  relexpfldd  15203  fsumcnv  15939  fprodcnv  16150  mrcun  17796  isacs1i  17831  mreacs  17832  arwval  18218  ipoval  18704  isacs5lem  18719  acsdrscl  18720  acsficl  18721  isps  18742  isdir  18772  qustrivr  19397  ghmqusnsglem1  19494  ghmquskerlem1  19497  ghmquskerco  19498  gicqusker  19502  pmtrval  19665  pmtrfv  19666  pmtrprfv  19667  pmtrdifellem3  19692  pmtrprfval  19701  gsumcom2  20189  dmdprd  20214  dprddisj  20225  dprdf1o  20248  dprdsn  20252  dprd2da  20258  dprd2db  20259  dmdprdsplit2lem  20261  lspuni0  21285  lss0v  21291  zrhval  21813  zrhval2  21814  zrhpropd  21820  isbasisg  23265  basis1  23268  baspartn  23272  tgval  23273  eltg  23275  ntrfval  23342  ntrval  23354  tgrest  23477  restuni2  23485  lmfval  23550  cnfval  23551  cnpfval  23552  pnrmopn  23661  fiuncmp  23722  cmpfi  23726  ptval  23889  ptpjpre1  23890  elptr2  23893  ptuni2  23895  ptbasin  23896  ptbasfi  23900  xkoval  23906  txtopon  23910  ptuni  23913  ptunimpt  23914  xkouni  23918  ptpjcn  23930  ptcld  23932  dfac14  23937  ptcnp  23941  prdstopn  23947  ptrescn  23958  txcmplem2  23961  xkoptsub  23973  xkopt  23974  qtopval  24014  qtopeu  24035  hmphindis  24116  txswaphmeolem  24123  ptuncnv  24126  ptunhmeo  24127  xpstopnlem1  24128  flimval  24282  fcfval  24352  alexsubALTlem3  24368  ptcmplem1  24371  ptcmplem2  24372  ptcmplem3  24373  ptcmplem4  24374  ptcmpg  24376  cnextfres1  24387  cldsubg  24430  utopval  24551  tusval  24584  tuslem  24585  tususs  24588  ucnval  24595  prdsxmslem2  24848  ishtpy  25293  pi1buni  25361  pi1xfrcnv  25378  elovolmr  25797  ovoliunlem3  25825  uniioombllem2  25904  uniioombllem3  25906  dyadmbl  25921  vmaval  27440  vmappw  27443  madeval  28218  oldval  28220  madeoldsuc  28271  unidifsnel  33131  unidifsnne  33132  disjabrex  33176  disjabrexf  33177  fnpreimac  33264  fcnvgreu  33266  xrge0tsmseq  33636  cycpm2tr  33680  lmicqusker  33969  ricqusker  33977  esplyfval1  34205  dimval  34233  dimvalfi  34234  algextdeglem4  34352  algextdeg  34357  locfinreflem  34472  locfinref  34473  pstmval  34527  pstmfval  34528  ordtprsuni  34551  esumeq12dvaf  34663  esumeq2  34668  esumval  34678  esumf1o  34682  esumsnf  34696  esumss  34704  esumpfinval  34707  esumpfinvalf  34708  sigapildsys  34795  sxsigon  34825  meascnbl  34852  brae  34874  braew  34875  faeval  34879  imambfm  34894  cnmbfm  34895  dya2iocuni  34915  omsval  34925  omsfval  34926  omsf  34928  oms0  34929  omssubaddlem  34931  omssubadd  34932  carsgval  34935  carsgclctunlem3  34952  omsmeas  34955  elprob  35041  probfinmeasb  35060  probmeasb  35062  dstrvprob  35104  fineqvnttrclselem1  35789  fineqvnttrclselem2  35790  fineqvnttrclselem3  35791  fineqvnttrclse  35792  fineqvr1ombregs  35806  wevgblacfn  35890  indispconn  35999  iscvm  36024  cvmscld  36038  msrfval  36302  msrval  36303  mthmpps  36347  rdgprc0  36555  rdgprc  36556  dfrdg2  36557  dfrdg3  36558  unisnif  36687  brapply  36700  cbviotadavw  37058  isfne  37127  fnemeet2  37155  fnejoin2  37157  tailfval  37160  ordcmp  37235  ttcid  37280  bj-imafv  38173  mptsnunlem  38262  dissneqlem  38264  ctbssinf  38330  ptrest  38538  mblfinlem2  38577  ovoliunnfl  38581  voliunnfl  38583  volsupnfl  38584  nfunidALT2  40027  nfunidALT  40028  mapdunirnN  42708  zndvdchrrhm  43024  aks6d1c7lem2  43232  aks5lem4a  43241  prjcrvfval  43668  aomclem8  44063  dfac21  44068  rp-unirabeq  44224  rp-tfslim  44355  oaun2  44383  oaun3  44384  ismnu  45245  mnuprdlem1  45256  mnuprdlem2  45257  grumnudlem  45269  grumnud  45270  ismnushort  45285  restuni6  46137  stoweidlem39  47049  salgenuni  47347  caragenval  47503  isome  47504  omeiunle  47527  isomennd  47541  unidmovn  47623  rrnmbl  47624  unidmvon  47627  hspmbl  47639  ovolval4lem2  47660  ovolval5lem2  47663  ovolval5lem3  47664  ovolval5  47665  ovnovollem2  47667  tmachlem-tpopen  47951  tmachlem-uassst  47953  afv2eq12d  48285  uniimaelsetpreimafv  48478  fundcmpsurinjlem3  48482  imasetpreimafvbijlemfo  48487  fundcmpsurbijinjpreimafv  48489  dftpos5  49982  tposideq  49996  restcls2lem  50021  mreclat  50105  toplatglb  50109  swapf1a  50377  swapf2a  50379  swapf1  50380  swapf2  50382  setrecseq  50788