Theorem unieqd 4944

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

Syntax hints:   → wi 4   = wceq 1537  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932

This theorem is referenced by:  unisn3  4952  csbuni  4960  unisn2  5330  opswap  6260  unixpid  6315  iotaeq  6538  iotabi  6539  uniabio  6540  iotanul  6551  funfv  7009  funfv2  7010  fvun  7012  dffv2  7017  fniunfv  7284  ordunisuc  7868  orduniss2  7869  onsucuni2  7870  elxp4  7962  elxp5  7963  1stval  8032  2ndval  8033  1stnpr  8034  2ndnpr  8035  fo1st  8050  fo2nd  8051  f1stres  8054  f2ndres  8055  1st2val  8058  2nd2val  8059  2nd1st  8079  cnvf1olem  8151  brtpos2  8273  dftpos4  8286  tpostpos  8287  frecseq123  8323  csbfrecsg  8325  wrecseq123OLD  8356  tz7.44-2  8463  tz7.44-3  8464  rdglim2  8488  ixpsnf1o  8996  xpcomco  9128  xpassen  9132  xpdom2  9133  supeq1  9514  supeq2  9517  supeq3  9518  supeq123d  9519  supval2  9524  rankuni  9932  en2other2  10078  dfac2a  10199  dfac12lem1  10213  dfac12r  10216  kmlem9  10228  kmlem11  10230  kmlem12  10231  enfin2i  10390  fin23lem29  10410  fin23lem30  10411  fin23lem32  10413  fin23lem34  10415  fin23lem35  10416  fin23lem36  10417  fin23lem38  10418  fin23lem39  10419  fin23lem41  10421  isf34lem7  10448  isf34lem6  10449  fin1a2lem10  10478  fin1a2lem11  10479  fin1a2lem12  10480  itunisuc  10488  itunitc  10490  ttukeylem3  10580  ttukey2g  10585  pwcfsdom  10652  gruurn  10867  dfinfre  12276  relexpfld  15098  relexpfldd  15099  fsumcnv  15821  fprodcnv  16031  mrcun  17680  isacs1i  17715  mreacs  17716  arwval  18110  ipoval  18600  isacs5lem  18615  acsdrscl  18616  acsficl  18617  isps  18638  isdir  18668  ghmqusnsglem1  19320  ghmquskerlem1  19323  ghmquskerco  19324  gicqusker  19328  pmtrval  19493  pmtrfv  19494  pmtrprfv  19495  pmtrdifellem3  19520  pmtrprfval  19529  gsumcom2  20017  dmdprd  20042  dprddisj  20053  dprdf1o  20076  dprdsn  20080  dprd2da  20086  dprd2db  20087  dmdprdsplit2lem  20089  lspuni0  21031  lss0v  21038  zrhval  21541  zrhval2  21542  zrhpropd  21548  isbasisg  22975  basis1  22978  baspartn  22982  tgval  22983  eltg  22985  ntrfval  23053  ntrval  23065  tgrest  23188  restuni2  23196  lmfval  23261  cnfval  23262  cnpfval  23263  pnrmopn  23372  fiuncmp  23433  cmpfi  23437  ptval  23599  ptpjpre1  23600  elptr2  23603  ptuni2  23605  ptbasin  23606  ptbasfi  23610  xkoval  23616  txtopon  23620  ptuni  23623  ptunimpt  23624  xkouni  23628  ptpjcn  23640  ptcld  23642  dfac14  23647  ptcnp  23651  prdstopn  23657  ptrescn  23668  txcmplem2  23671  xkoptsub  23683  xkopt  23684  qtopval  23724  qtopeu  23745  hmphindis  23826  txswaphmeolem  23833  ptuncnv  23836  ptunhmeo  23837  xpstopnlem1  23838  flimval  23992  fcfval  24062  alexsubALTlem3  24078  ptcmplem1  24081  ptcmplem2  24082  ptcmplem3  24083  ptcmplem4  24084  ptcmpg  24086  cnextfres1  24097  cldsubg  24140  utopval  24262  tusval  24295  tuslem  24296  tuslemOLD  24297  tususs  24300  ucnval  24307  prdsxmslem2  24563  ishtpy  25023  pi1buni  25092  pi1xfrcnv  25109  elovolmr  25530  ovoliunlem3  25558  uniioombllem2  25637  uniioombllem3  25639  dyadmbl  25654  vmaval  27174  vmappw  27177  madeval  27909  oldval  27911  madeoldsuc  27941  zs12bday  28442  unidifsnel  32563  unidifsnne  32564  disjabrex  32604  disjabrexf  32605  fnpreimac  32689  fcnvgreu  32691  xrge0tsmseq  33043  cycpm2tr  33112  qustrivr  33358  lmicqusker  33411  ricqusker  33420  dimval  33613  dimvalfi  33614  algextdeglem4  33711  algextdeg  33716  locfinreflem  33786  locfinref  33787  pstmval  33841  pstmfval  33842  ordtprsuni  33865  esumeq12dvaf  33995  esumeq2  34000  esumval  34010  esumf1o  34014  esumsnf  34028  esumss  34036  esumpfinval  34039  esumpfinvalf  34040  sigapildsys  34126  sxsigon  34156  meascnbl  34183  brae  34205  braew  34206  faeval  34210  imambfm  34227  cnmbfm  34228  dya2iocuni  34248  omsval  34258  omsfval  34259  omsf  34261  oms0  34262  omssubaddlem  34264  omssubadd  34265  carsgval  34268  carsgclctunlem3  34285  omsmeas  34288  elprob  34374  probfinmeasb  34393  probmeasb  34395  dstrvprob  34436  wevgblacfn  35076  indispconn  35202  iscvm  35227  cvmscld  35241  msrfval  35505  msrval  35506  mthmpps  35550  rdgprc0  35757  rdgprc  35758  dfrdg2  35759  dfrdg3  35760  unisnif  35889  brapply  35902  cbviotadavw  36235  isfne  36305  fnemeet2  36333  fnejoin2  36335  tailfval  36338  ordcmp  36413  bj-imafv  37217  mptsnunlem  37304  dissneqlem  37306  ctbssinf  37372  ptrest  37579  mblfinlem2  37618  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  nfunidALT2  38925  nfunidALT  38926  mapdunirnN  41607  zndvdchrrhm  41927  aks6d1c7lem2  42138  aks5lem4a  42147  prjcrvfval  42586  aomclem8  43018  dfac21  43023  rp-unirabeq  43183  rp-tfslim  43315  oaun2  43343  oaun3  43344  ismnu  44230  mnuprdlem1  44241  mnuprdlem2  44242  grumnudlem  44254  grumnud  44255  ismnushort  44270  restuni6  45024  stoweidlem39  45960  salgenuni  46258  caragenval  46414  isome  46415  omeiunle  46438  isomennd  46452  unidmovn  46534  rrnmbl  46535  unidmvon  46538  hspmbl  46550  ovolval4lem2  46571  ovolval5lem2  46574  ovolval5lem3  46575  ovolval5  46576  ovnovollem2  46578  afv2eq12d  47130  uniimaelsetpreimafv  47270  fundcmpsurinjlem3  47274  imasetpreimafvbijlemfo  47279  fundcmpsurbijinjpreimafv  47281  restcls2lem  48592  mreclat  48669  toplatglb  48673  setrecseq  48777