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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-uni 4841

This theorem is referenced by:  uniprg  4858  unisn3  4861  csbuni  4869  unisn2  5218  opswap  6088  unixpid  6137  iotaeq  6328  iotabi  6329  uniabio  6330  iotanul  6335  funfv  6752  funfv2  6753  fvun  6755  dffv2  6758  fniunfv  7008  ordunisuc  7549  orduniss2  7550  onsucuni2  7551  elxp4  7629  elxp5  7630  1stval  7693  2ndval  7694  1stnpr  7695  2ndnpr  7696  fo1st  7711  fo2nd  7712  f1stres  7715  f2ndres  7716  1st2val  7719  2nd2val  7720  2nd1st  7739  cnvf1olem  7807  brtpos2  7900  dftpos4  7913  tpostpos  7914  wrecseq123  7950  tz7.44-2  8045  tz7.44-3  8046  rdglim2  8070  ixpsnf1o  8504  xpcomco  8609  xpassen  8613  xpdom2  8614  supeq1  8911  supeq2  8914  supeq3  8915  supeq123d  8916  supval2  8921  rankuni  9294  en2other2  9437  dfac2a  9557  dfac12lem1  9571  dfac12r  9574  kmlem9  9586  kmlem11  9588  kmlem12  9589  enfin2i  9745  fin23lem29  9765  fin23lem30  9766  fin23lem32  9768  fin23lem34  9770  fin23lem35  9771  fin23lem36  9772  fin23lem38  9773  fin23lem39  9774  fin23lem41  9776  isf34lem7  9803  isf34lem6  9804  fin1a2lem10  9833  fin1a2lem11  9834  fin1a2lem12  9835  itunisuc  9843  itunitc  9845  ttukeylem3  9935  ttukey2g  9940  pwcfsdom  10007  gruurn  10222  dfinfre  11624  relexpfld  14410  fsumcnv  15130  fprodcnv  15339  mrcun  16895  isacs1i  16930  mreacs  16931  arwval  17305  ipoval  17766  isacs5lem  17781  acsdrscl  17782  acsficl  17783  isps  17814  isdir  17844  pmtrval  18581  pmtrfv  18582  pmtrprfv  18583  pmtrdifellem3  18608  pmtrprfval  18617  gsumcom2  19097  dmdprd  19122  dprddisj  19133  dprdf1o  19156  dprdsn  19160  dprd2da  19166  dprd2db  19167  dmdprdsplit2lem  19169  lspuni0  19784  lss0v  19790  zrhval  20657  zrhval2  20658  zrhpropd  20664  isbasisg  21557  basis1  21560  baspartn  21564  tgval  21565  eltg  21567  ntrfval  21634  ntrval  21646  tgrest  21769  restuni2  21777  lmfval  21842  cnfval  21843  cnpfval  21844  pnrmopn  21953  fiuncmp  22014  cmpfi  22018  ptval  22180  ptpjpre1  22181  elptr2  22184  ptuni2  22186  ptbasin  22187  ptbasfi  22191  xkoval  22197  txtopon  22201  ptuni  22204  ptunimpt  22205  xkouni  22209  ptpjcn  22221  ptcld  22223  dfac14  22228  ptcnp  22232  prdstopn  22238  ptrescn  22249  txcmplem2  22252  xkoptsub  22264  xkopt  22265  qtopval  22305  qtopeu  22326  hmphindis  22407  txswaphmeolem  22414  ptuncnv  22417  ptunhmeo  22418  xpstopnlem1  22419  flimval  22573  fcfval  22643  alexsubALTlem3  22659  ptcmplem1  22662  ptcmplem2  22663  ptcmplem3  22664  ptcmplem4  22665  ptcmpg  22667  cnextfres1  22678  cldsubg  22721  utopval  22843  tusval  22877  tuslem  22878  tususs  22881  ucnval  22888  prdsxmslem2  23141  ishtpy  23578  pi1buni  23646  pi1xfrcnv  23663  elovolmr  24079  ovoliunlem3  24107  uniioombllem2  24186  uniioombllem3  24188  dyadmbl  24203  vmaval  25692  vmappw  25695  unidifsnel  30297  unidifsnne  30298  disjabrex  30334  disjabrexf  30335  fnpreimac  30418  fcnvgreu  30420  xrge0tsmseq  30696  cycpm2tr  30763  qustrivr  30932  dimval  31003  dimvalfi  31004  locfinreflem  31106  locfinref  31107  pstmval  31137  pstmfval  31138  ordtprsuni  31164  esumeq12dvaf  31292  esumeq2  31297  esumval  31307  esumf1o  31311  esumsnf  31325  esumss  31333  esumpfinval  31336  esumpfinvalf  31337  sigapildsys  31423  sxsigon  31453  meascnbl  31480  brae  31502  braew  31503  faeval  31507  imambfm  31522  cnmbfm  31523  dya2iocuni  31543  omsval  31553  omsfval  31554  omsf  31556  oms0  31557  omssubaddlem  31559  omssubadd  31560  carsgval  31563  carsgclctunlem3  31580  omsmeas  31583  elprob  31669  probfinmeasb  31688  probmeasb  31690  dstrvprob  31731  indispconn  32483  iscvm  32508  cvmscld  32522  msrfval  32786  msrval  32787  mthmpps  32831  rdgprc0  33040  rdgprc  33041  dfrdg2  33042  dfrdg3  33043  trpredeq1  33061  trpredeq2  33062  trpredeq3  33063  frecseq123  33121  madeval  33291  unisnif  33388  brapply  33401  isfne  33689  fnemeet2  33717  fnejoin2  33719  tailfval  33722  ordcmp  33797  bj-imafv  34535  csbwrecsg  34610  mptsnunlem  34621  dissneqlem  34623  ctbssinf  34689  ptrest  34893  mblfinlem2  34932  ovoliunnfl  34936  voliunnfl  34938  volsupnfl  34939  nfunidALT2  36107  nfunidALT  36108  mapdunirnN  38788  aomclem8  39668  dfac21  39673  ismnu  40604  mnuprdlem1  40615  mnuprdlem2  40616  grumnudlem  40628  grumnud  40629  restuni6  41395  stoweidlem39  42331  salgenuni  42627  caragenval  42782  isome  42783  omeiunle  42806  isomennd  42820  unidmovn  42902  rrnmbl  42903  unidmvon  42906  hspmbl  42918  ovolval4lem2  42939  ovolval5lem2  42942  ovolval5lem3  42943  ovolval5  42944  ovnovollem2  42946  afv2eq12d  43421  uniimaelsetpreimafv  43563  fundcmpsurinjlem3  43567  imasetpreimafvbijlemfo  43572  fundcmpsurbijinjpreimafv  43574  setrecseq  44795