Theorem unieqd 4761

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

Syntax hints:   → wi 4   = wceq 1525  ∪ cuni 4751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-rex 3113  df-uni 4752

This theorem is referenced by:  uniprg  4765  unisn3  4768  csbuni  4779  unisn2  5114  opswap  5968  unixpid  6017  iotaeq  6204  iotabi  6205  uniabio  6206  iotanul  6211  funfv  6624  funfv2  6625  fvun  6627  dffv2  6630  fniunfv  6878  ordunisuc  7410  orduniss2  7411  onsucuni2  7412  elxp4  7490  elxp5  7491  1stval  7554  2ndval  7555  1stnpr  7556  2ndnpr  7557  fo1st  7572  fo2nd  7573  f1stres  7576  f2ndres  7577  1st2val  7580  2nd2val  7581  2nd1st  7600  cnvf1olem  7668  brtpos2  7756  dftpos4  7769  tpostpos  7770  wrecseq123  7806  tz7.44-2  7902  tz7.44-3  7903  rdglim2  7927  ixpsnf1o  8357  xpcomco  8461  xpassen  8465  xpdom2  8466  supeq1  8762  supeq2  8765  supeq3  8766  supeq123d  8767  supval2  8772  rankuni  9145  en2other2  9288  dfac2a  9408  dfac12lem1  9422  dfac12r  9425  kmlem9  9437  kmlem11  9439  kmlem12  9440  enfin2i  9596  fin23lem29  9616  fin23lem30  9617  fin23lem32  9619  fin23lem34  9621  fin23lem35  9622  fin23lem36  9623  fin23lem38  9624  fin23lem39  9625  fin23lem41  9627  isf34lem7  9654  isf34lem6  9655  fin1a2lem10  9684  fin1a2lem11  9685  fin1a2lem12  9686  itunisuc  9694  itunitc  9696  ttukeylem3  9786  ttukey2g  9791  pwcfsdom  9858  gruurn  10073  dfinfre  11476  relexpfld  14246  fsumcnv  14965  fprodcnv  15174  mrcun  16726  isacs1i  16761  mreacs  16762  arwval  17136  ipoval  17597  isacs5lem  17612  acsdrscl  17613  acsficl  17614  isps  17645  isdir  17675  pmtrval  18314  pmtrfv  18315  pmtrprfv  18316  pmtrdifellem3  18341  pmtrprfval  18350  gsumcom2  18819  dmdprd  18841  dprddisj  18852  dprdf1o  18875  dprdsn  18879  dprd2da  18885  dprd2db  18886  dmdprdsplit2lem  18888  lspuni0  19476  lss0v  19482  zrhval  20341  zrhval2  20342  zrhpropd  20348  isbasisg  21243  basis1  21246  baspartn  21250  tgval  21251  eltg  21253  ntrfval  21320  ntrval  21332  tgrest  21455  restuni2  21463  lmfval  21528  cnfval  21529  cnpfval  21530  pnrmopn  21639  fiuncmp  21700  cmpfi  21704  ptval  21866  ptpjpre1  21867  elptr2  21870  ptuni2  21872  ptbasin  21873  ptbasfi  21877  xkoval  21883  txtopon  21887  ptuni  21890  ptunimpt  21891  xkouni  21895  ptpjcn  21907  ptcld  21909  dfac14  21914  ptcnp  21918  prdstopn  21924  ptrescn  21935  txcmplem2  21938  xkoptsub  21950  xkopt  21951  qtopval  21991  qtopeu  22012  hmphindis  22093  txswaphmeolem  22100  ptuncnv  22103  ptunhmeo  22104  xpstopnlem1  22105  flimval  22259  fcfval  22329  alexsubALTlem3  22345  ptcmplem1  22348  ptcmplem2  22349  ptcmplem3  22350  ptcmplem4  22351  ptcmpg  22353  cnextfres1  22364  cldsubg  22406  utopval  22528  tusval  22562  tuslem  22563  tususs  22566  ucnval  22573  prdsxmslem2  22826  ishtpy  23263  pi1buni  23331  pi1xfrcnv  23348  elovolmr  23764  ovoliunlem3  23792  uniioombllem2  23871  uniioombllem3  23873  dyadmbl  23888  vmaval  25376  vmappw  25379  unidifsnel  29980  unidifsnne  29981  disjabrex  30018  disjabrexf  30019  fnpreimac  30102  fcnvgreu  30104  cycpm2tr  30404  xrge0tsmseq  30501  dimval  30601  dimvalfi  30602  locfinreflem  30717  locfinref  30718  pstmval  30748  pstmfval  30749  ordtprsuni  30775  esumeq12dvaf  30903  esumeq2  30908  esumval  30918  esumf1o  30922  esumsnf  30936  esumss  30944  esumpfinval  30947  esumpfinvalf  30948  sigapildsys  31034  sxsigon  31064  meascnbl  31091  brae  31113  braew  31114  faeval  31118  imambfm  31133  cnmbfm  31134  dya2iocuni  31154  omsval  31164  omsfval  31165  omsf  31167  oms0  31168  omssubaddlem  31170  omssubadd  31171  carsgval  31174  carsgclctunlem3  31191  omsmeas  31194  elprob  31280  probfinmeasb  31299  probmeasb  31301  dstrvprob  31342  indispconn  32091  iscvm  32116  cvmscld  32130  msrfval  32394  msrval  32395  mthmpps  32439  rdgprc0  32649  rdgprc  32650  dfrdg2  32651  dfrdg3  32652  trpredeq1  32670  trpredeq2  32671  trpredeq3  32672  frecseq123  32730  madeval  32900  unisnif  32997  brapply  33010  isfne  33298  fnemeet2  33326  fnejoin2  33328  tailfval  33331  ordcmp  33406  bj-imafv  34112  csbwrecsg  34160  mptsnunlem  34171  dissneqlem  34173  ctbssinf  34239  ptrest  34443  mblfinlem2  34482  ovoliunnfl  34486  voliunnfl  34488  volsupnfl  34489  nfunidALT2  35657  nfunidALT  35658  mapdunirnN  38338  aomclem8  39167  dfac21  39172  ismnu  40115  mnuprdlem1  40126  mnuprdlem2  40127  grumnudlem  40139  grumnud  40140  restuni6  40949  stoweidlem39  41888  salgenuni  42184  caragenval  42339  isome  42340  omeiunle  42363  isomennd  42377  unidmovn  42459  rrnmbl  42460  unidmvon  42463  hspmbl  42475  ovolval4lem2  42496  ovolval5lem2  42499  ovolval5lem3  42500  ovolval5  42501  ovnovollem2  42503  afv2eq12d  42952  setrecseq  44290