Theorem unieqd 4584

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

Syntax hints:   → wi 4   = wceq 1631  ∪ cuni 4574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-uni 4575

This theorem is referenced by:  uniprg  4588  unisng  4590  unisn3  4591  csbuni  4602  unisn2  4928  opswap  5766  unixpid  5814  iotaeq  6002  iotabi  6003  uniabio  6004  iotanul  6009  funfv  6407  funfv2  6408  fvun  6410  dffv2  6413  fniunfv  6648  ordunisuc  7179  orduniss2  7180  onsucuni2  7181  elxp4  7257  elxp5  7258  1stval  7317  2ndval  7318  1stnpr  7319  2ndnpr  7320  fo1st  7335  fo2nd  7336  f1stres  7339  f2ndres  7340  1st2val  7343  2nd2val  7344  2nd1st  7362  cnvf1olem  7426  brtpos2  7510  dftpos4  7523  tpostpos  7524  wrecseq123  7560  tz7.44-2  7656  tz7.44-3  7657  rdglim2  7681  ixpsnf1o  8102  xpcomco  8206  xpassen  8210  xpdom2  8211  supeq1  8507  supeq2  8510  supeq3  8511  supeq123d  8512  supval2  8517  rankuni  8890  en2other2  9032  dfac2a  9152  dfac12lem1  9167  dfac12r  9170  kmlem9  9182  kmlem11  9184  kmlem12  9185  enfin2i  9345  fin23lem29  9365  fin23lem30  9366  fin23lem32  9368  fin23lem34  9370  fin23lem35  9371  fin23lem36  9372  fin23lem38  9373  fin23lem39  9374  fin23lem41  9376  isf34lem7  9403  isf34lem6  9404  fin1a2lem10  9433  fin1a2lem11  9434  fin1a2lem12  9435  itunisuc  9443  itunitc  9445  ttukeylem3  9535  ttukey2g  9540  pwcfsdom  9607  gruurn  9822  dfinfre  11206  relexpfld  13997  fsumcnv  14712  fprodcnv  14920  mrcun  16490  isacs1i  16525  mreacs  16526  arwval  16900  ipoval  17362  isacs5lem  17377  acsdrscl  17378  acsficl  17379  isps  17410  isdir  17440  pmtrval  18078  pmtrfv  18079  pmtrprfv  18080  pmtrdifellem3  18105  pmtrprfval  18114  gsumcom2  18581  dmdprd  18605  dprddisj  18616  dprdf1o  18639  dprdsn  18643  dprd2da  18649  dprd2db  18650  dmdprdsplit2lem  18652  lspuni0  19223  lss0v  19229  zrhval  20071  zrhval2  20072  zrhpropd  20078  isbasisg  20972  basis1  20975  baspartn  20979  tgval  20980  eltg  20982  ntrfval  21049  ntrval  21061  tgrest  21184  restuni2  21192  lmfval  21257  cnfval  21258  cnpfval  21259  pnrmopn  21368  fiuncmp  21428  cmpfi  21432  ptval  21594  ptpjpre1  21595  elptr2  21598  ptuni2  21600  ptbasin  21601  ptbasfi  21605  xkoval  21611  txtopon  21615  ptuni  21618  ptunimpt  21619  xkouni  21623  ptpjcn  21635  ptcld  21637  dfac14  21642  ptcnp  21646  prdstopn  21652  ptrescn  21663  txcmplem2  21666  xkoptsub  21678  xkopt  21679  qtopval  21719  qtopeu  21740  hmphindis  21821  txswaphmeolem  21828  ptuncnv  21831  ptunhmeo  21832  xpstopnlem1  21833  flimval  21987  fcfval  22057  alexsubALTlem3  22073  ptcmplem1  22076  ptcmplem2  22077  ptcmplem3  22078  ptcmplem4  22079  ptcmpg  22081  cnextfres1  22092  cldsubg  22134  utopval  22256  tusval  22290  tuslem  22291  tususs  22294  ucnval  22301  prdsxmslem2  22554  ishtpy  22991  pi1buni  23059  pi1xfrcnv  23076  elovolmr  23464  ovoliunlem3  23492  uniioombllem2  23571  uniioombllem3  23573  dyadmbl  23588  vmaval  25060  vmappw  25063  disjabrex  29733  disjabrexf  29734  fcnvgreu  29812  xrge0tsmseq  30127  locfinreflem  30247  locfinref  30248  pstmval  30278  pstmfval  30279  ordtprsuni  30305  esumeq12dvaf  30433  esumeq2  30438  esumval  30448  esumf1o  30452  esumsnf  30466  esumss  30474  esumpfinval  30477  esumpfinvalf  30478  sigapildsys  30565  sxsigon  30595  meascnbl  30622  brae  30644  braew  30645  faeval  30649  imambfm  30664  cnmbfm  30665  dya2iocuni  30685  omsval  30695  omsfval  30696  omsf  30698  oms0  30699  omssubaddlem  30701  omssubadd  30702  carsgval  30705  carsgclctunlem3  30722  omsmeas  30725  elprob  30811  probfinmeasb  30831  probmeasb  30832  dstrvprob  30873  indispconn  31554  iscvm  31579  cvmscld  31593  msrfval  31772  msrval  31773  mthmpps  31817  rdgprc0  32035  rdgprc  32036  dfrdg2  32037  dfrdg3  32038  trpredeq1  32056  trpredeq2  32057  trpredeq3  32058  frecseq123  32114  madeval  32272  unisnif  32369  brapply  32382  isfne  32671  fnemeet2  32699  fnejoin2  32701  tailfval  32704  ordcmp  32783  csbwrecsg  33510  mptsnunlem  33522  dissneqlem  33524  ptrest  33741  mblfinlem2  33780  ovoliunnfl  33784  voliunnfl  33786  volsupnfl  33787  nfunidALT2  34778  nfunidALT  34779  mapdunirnN  37460  aomclem8  38157  dfac21  38162  restuni6  39826  stoweidlem39  40773  salgenuni  41072  caragenval  41227  isome  41228  omeiunle  41251  isomennd  41265  unidmovn  41347  rrnmbl  41348  unidmvon  41351  hspmbl  41363  ovolval4lem2  41384  ovolval5lem2  41387  ovolval5lem3  41388  ovolval5  41389  ovnovollem2  41391  setrecseq  42960