Theorem unieqd 4883

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ∪ cuni 4870

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871

This theorem is used by:  unisn3  4891  csbuni  4901  unisn2  5269  opswap  6242  unixpid  6302  iotaeq  6521  iotabi  6522  uniabio  6523  iotanul  6534  funfv  6992  funfv2  6993  fvun  6995  dffv2  7000  fniunfv  7271  ordunisuc  7864  orduniss2  7865  onsucuni2  7866  elxp4  7955  elxp5  7956  1stval  8024  2ndval  8025  1stnpr  8026  2ndnpr  8027  fo1st  8042  fo2nd  8043  f1stres  8046  f2ndres  8047  1st2val  8050  2nd2val  8051  2nd1st  8070  cnvf1olem  8145  brtpos2  8274  dftpos4  8287  tpostpos  8288  frecseq123  8325  csbfrecsg  8327  tz7.44-2  8440  tz7.44-3  8441  rdglim2  8465  ixpsnf1o  8991  xpcomco  9111  xpassen  9115  xpdom2  9116  supeq1  9461  supeq2  9464  supeq3  9465  supeq123d  9466  supval2  9471  rankuni  9903  en2other2  10112  dfac2a  10232  dfac12lem1  10246  dfac12r  10249  kmlem9  10261  kmlem11  10263  kmlem12  10264  enfin2i  10423  fin23lem29  10443  fin23lem30  10444  fin23lem32  10446  fin23lem34  10448  fin23lem35  10449  fin23lem36  10450  fin23lem38  10451  fin23lem39  10452  fin23lem41  10454  isf34lem7  10481  isf34lem6  10482  fin1a2lem10  10511  fin1a2lem11  10512  fin1a2lem12  10513  itunisuc  10521  itunitc  10523  ttukeylem3  10613  ttukey2g  10618  pwcfsdom  10692  gruurn  10907  dfinfre  12322  relexpfld  15228  relexpfldd  15229  fsumcnv  15965  fprodcnv  16176  mrcun  17822  isacs1i  17857  mreacs  17858  arwval  18244  ipoval  18730  isacs5lem  18745  acsdrscl  18746  acsficl  18747  isps  18768  isdir  18798  qustrivr  19423  ghmqusnsglem1  19521  ghmquskerlem1  19524  ghmquskerco  19525  gicqusker  19529  pmtrval  19692  pmtrfv  19693  pmtrprfv  19694  pmtrdifellem3  19719  pmtrprfval  19728  gsumcom2  20216  dmdprd  20241  dprddisj  20252  dprdf1o  20275  dprdsn  20279  dprd2da  20285  dprd2db  20286  dmdprdsplit2lem  20288  lspuni0  21312  lss0v  21318  zrhval  21840  zrhval2  21841  zrhpropd  21847  isbasisg  23292  basis1  23295  baspartn  23299  tgval  23300  eltg  23302  ntrfval  23369  ntrval  23381  tgrest  23504  restuni2  23512  lmfval  23577  cnfval  23578  cnpfval  23579  pnrmopn  23688  fiuncmp  23749  cmpfi  23753  ptval  23916  ptpjpre1  23917  elptr2  23920  ptuni2  23922  ptbasin  23923  ptbasfi  23927  xkoval  23933  txtopon  23937  ptuni  23940  ptunimpt  23941  xkouni  23945  ptpjcn  23957  ptcld  23959  dfac14  23964  ptcnp  23968  prdstopn  23974  ptrescn  23985  txcmplem2  23988  xkoptsub  24000  xkopt  24001  qtopval  24041  qtopeu  24062  hmphindis  24143  txswaphmeolem  24150  ptuncnv  24153  ptunhmeo  24154  xpstopnlem1  24155  flimval  24309  fcfval  24379  alexsubALTlem3  24395  ptcmplem1  24398  ptcmplem2  24399  ptcmplem3  24400  ptcmplem4  24401  ptcmpg  24403  cnextfres1  24414  cldsubg  24457  utopval  24578  tusval  24611  tuslem  24612  tususs  24615  ucnval  24622  prdsxmslem2  24875  ishtpy  25320  pi1buni  25388  pi1xfrcnv  25405  elovolmr  25824  ovoliunlem3  25852  uniioombllem2  25931  uniioombllem3  25933  dyadmbl  25948  vmaval  27467  vmappw  27470  madeval  28245  oldval  28247  madeoldsuc  28298  unidifsnel  33200  unidifsnne  33201  disjabrex  33245  disjabrexf  33246  fnpreimac  33333  fcnvgreu  33335  xrge0tsmseq  33703  cycpm2tr  33747  lmicqusker  34036  ricqusker  34044  esplyfval1  34272  dimval  34300  dimvalfi  34301  algextdeglem4  34419  algextdeg  34424  locfinreflem  34539  locfinref  34540  pstmval  34594  pstmfval  34595  ordtprsuni  34618  esumeq12dvaf  34730  esumeq2  34735  esumval  34745  esumf1o  34749  esumsnf  34763  esumss  34771  esumpfinval  34774  esumpfinvalf  34775  sigapildsys  34862  sxsigon  34892  meascnbl  34919  brae  34941  braew  34942  faeval  34946  imambfm  34961  cnmbfm  34962  dya2iocuni  34982  omsval  34992  omsfval  34993  omsf  34995  oms0  34996  omssubaddlem  34998  omssubadd  34999  carsgval  35002  carsgclctunlem3  35019  omsmeas  35022  elprob  35108  probfinmeasb  35127  probmeasb  35129  dstrvprob  35171  fineqvnttrclselem1  35888  fineqvnttrclselem2  35889  fineqvnttrclselem3  35890  fineqvnttrclse  35891  fineqvr1ombregs  35905  wevgblacfn  36038  indispconn  36165  iscvm  36190  cvmscld  36204  msrfval  36468  msrval  36469  mthmpps  36513  rdgprc0  36732  rdgprc  36733  dfrdg2  36734  dfrdg3  36735  unisnif  36864  brapply  36877  cbviotadavw  37235  isfne  37304  fnemeet2  37332  fnejoin2  37334  tailfval  37337  ordcmp  37412  ttcid  37457  bj-imafv  38363  mptsnunlem  38452  dissneqlem  38454  ctbssinf  38520  ptrest  38728  mblfinlem2  38767  ovoliunnfl  38771  voliunnfl  38773  volsupnfl  38774  nfunidALT2  40217  nfunidALT  40218  mapdunirnN  42898  zndvdchrrhm  43214  aks6d1c7lem2  43422  aks5lem4a  43431  prjcrvfval  43858  aomclem8  44254  dfac21  44259  rp-unirabeq  44414  rp-tfslim  44545  oaun2  44573  oaun3  44574  ismnu  45435  mnuprdlem1  45446  mnuprdlem2  45447  grumnudlem  45459  grumnud  45460  ismnushort  45475  restuni6  46340  stoweidlem39  47252  salgenuni  47550  caragenval  47706  isome  47707  omeiunle  47730  isomennd  47744  unidmovn  47826  rrnmbl  47827  unidmvon  47830  hspmbl  47842  ovolval4lem2  47863  ovolval5lem2  47866  ovolval5lem3  47867  ovolval5  47868  ovnovollem2  47870  tmachlem-tpopen  48154  tmachlem-uassst  48156  afv2eq12d  48488  uniimaelsetpreimafv  48681  fundcmpsurinjlem3  48685  imasetpreimafvbijlemfo  48690  fundcmpsurbijinjpreimafv  48692  dftpos5  50190  tposideq  50204  restcls2lem  50230  mreclat  50314  toplatglb  50318  swapf1a  50594  swapf2a  50596  swapf1  50597  swapf2  50599  setrecseq  51066