Theorem unieqd 4887

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

Syntax hints:   → wi 4   = wceq 1567  ∪ cuni 4874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3463  df-ss 3928  df-uni 4875

This theorem is referenced by:  unisn3  4895  csbuni  4905  unisn2  5277  opswap  6231  unixpid  6286  iotaeq  6505  iotabi  6506  uniabio  6507  iotanul  6517  funfv  6969  funfv2  6970  fvun  6972  dffv2  6977  fniunfv  7246  ordunisuc  7828  orduniss2  7829  onsucuni2  7830  elxp4  7919  elxp5  7920  1stval  7988  2ndval  7989  1stnpr  7990  2ndnpr  7991  fo1st  8006  fo2nd  8007  f1stres  8010  f2ndres  8011  1st2val  8014  2nd2val  8015  2nd1st  8035  cnvf1olem  8105  brtpos2  8228  dftpos4  8241  tpostpos  8242  frecseq123  8279  csbfrecsg  8281  tz7.44-2  8394  tz7.44-3  8395  rdglim2  8419  ixpsnf1o  8936  xpcomco  9055  xpassen  9059  xpdom2  9060  supeq1  9405  supeq2  9408  supeq3  9409  supeq123d  9410  supval2  9415  rankuni  9835  en2other2  9993  dfac2a  10113  dfac12lem1  10127  dfac12r  10130  kmlem9  10142  kmlem11  10144  kmlem12  10145  enfin2i  10305  fin23lem29  10325  fin23lem30  10326  fin23lem32  10328  fin23lem34  10330  fin23lem35  10331  fin23lem36  10332  fin23lem38  10333  fin23lem39  10334  fin23lem41  10336  isf34lem7  10363  isf34lem6  10364  fin1a2lem10  10393  fin1a2lem11  10394  fin1a2lem12  10395  itunisuc  10403  itunitc  10405  ttukeylem3  10495  ttukey2g  10500  pwcfsdom  10568  gruurn  10783  dfinfre  12196  relexpfld  15086  relexpfldd  15087  fsumcnv  15824  fprodcnv  16037  mrcun  17678  isacs1i  17713  mreacs  17714  arwval  18100  ipoval  18586  isacs5lem  18601  acsdrscl  18602  acsficl  18603  isps  18624  isdir  18654  qustrivr  19253  ghmqusnsglem1  19350  ghmquskerlem1  19353  ghmquskerco  19354  gicqusker  19358  pmtrval  19521  pmtrfv  19522  pmtrprfv  19523  pmtrdifellem3  19548  pmtrprfval  19557  gsumcom2  20045  dmdprd  20070  dprddisj  20081  dprdf1o  20104  dprdsn  20108  dprd2da  20114  dprd2db  20115  dmdprdsplit2lem  20117  lspuni0  21109  lss0v  21115  zrhval  21626  zrhval2  21627  zrhpropd  21633  isbasisg  23073  basis1  23076  baspartn  23080  tgval  23081  eltg  23083  ntrfval  23150  ntrval  23162  tgrest  23285  restuni2  23293  lmfval  23358  cnfval  23359  cnpfval  23360  pnrmopn  23469  fiuncmp  23530  cmpfi  23534  ptval  23696  ptpjpre1  23697  elptr2  23700  ptuni2  23702  ptbasin  23703  ptbasfi  23707  xkoval  23713  txtopon  23717  ptuni  23720  ptunimpt  23721  xkouni  23725  ptpjcn  23737  ptcld  23739  dfac14  23744  ptcnp  23748  prdstopn  23754  ptrescn  23765  txcmplem2  23768  xkoptsub  23780  xkopt  23781  qtopval  23821  qtopeu  23842  hmphindis  23923  txswaphmeolem  23930  ptuncnv  23933  ptunhmeo  23934  xpstopnlem1  23935  flimval  24089  fcfval  24159  alexsubALTlem3  24175  ptcmplem1  24178  ptcmplem2  24179  ptcmplem3  24180  ptcmplem4  24181  ptcmpg  24183  cnextfres1  24194  cldsubg  24237  utopval  24358  tusval  24391  tuslem  24392  tususs  24395  ucnval  24402  prdsxmslem2  24655  ishtpy  25100  pi1buni  25168  pi1xfrcnv  25185  elovolmr  25604  ovoliunlem3  25632  uniioombllem2  25711  uniioombllem3  25713  dyadmbl  25728  vmaval  27243  vmappw  27246  madeval  27991  oldval  27993  madeoldsuc  28044  unidifsnel  32822  unidifsnne  32823  disjabrex  32868  disjabrexf  32869  fnpreimac  32956  fcnvgreu  32958  xrge0tsmseq  33336  cycpm2tr  33380  lmicqusker  33671  ricqusker  33679  esplyfval1  33908  dimval  33936  dimvalfi  33937  algextdeglem4  34055  algextdeg  34060  locfinreflem  34175  locfinref  34176  pstmval  34230  pstmfval  34231  ordtprsuni  34254  esumeq12dvaf  34366  esumeq2  34371  esumval  34381  esumf1o  34385  esumsnf  34399  esumss  34407  esumpfinval  34410  esumpfinvalf  34411  sigapildsys  34497  sxsigon  34527  meascnbl  34554  brae  34576  braew  34577  faeval  34581  imambfm  34597  cnmbfm  34598  dya2iocuni  34618  omsval  34628  omsfval  34629  omsf  34631  oms0  34632  omssubaddlem  34634  omssubadd  34635  carsgval  34638  carsgclctunlem3  34655  omsmeas  34658  elprob  34744  probfinmeasb  34763  probmeasb  34765  dstrvprob  34807  fineqvnttrclselem1  35467  fineqvnttrclselem2  35468  fineqvnttrclselem3  35469  fineqvnttrclse  35470  fineqvr1ombregs  35484  wevgblacfn  35528  indispconn  35659  iscvm  35684  cvmscld  35698  msrfval  35962  msrval  35963  mthmpps  36007  rdgprc0  36216  rdgprc  36217  dfrdg2  36218  dfrdg3  36219  unisnif  36348  brapply  36361  cbviotadavw  36704  isfne  36773  fnemeet2  36801  fnejoin2  36803  tailfval  36806  ordcmp  36881  ttcid  36926  bj-imafv  37818  mptsnunlem  37907  dissneqlem  37909  ctbssinf  37975  ptrest  38193  mblfinlem2  38232  ovoliunnfl  38236  voliunnfl  38238  volsupnfl  38239  nfunidALT2  39668  nfunidALT  39669  mapdunirnN  42349  zndvdchrrhm  42665  aks6d1c7lem2  42873  aks5lem4a  42882  prjcrvfval  43290  aomclem8  43715  dfac21  43720  rp-unirabeq  43876  rp-tfslim  44007  oaun2  44035  oaun3  44036  ismnu  44898  mnuprdlem1  44909  mnuprdlem2  44910  grumnudlem  44922  grumnud  44923  ismnushort  44938  restuni6  45767  stoweidlem39  46680  salgenuni  46978  caragenval  47134  isome  47135  omeiunle  47158  isomennd  47172  unidmovn  47254  rrnmbl  47255  unidmvon  47258  hspmbl  47270  ovolval4lem2  47291  ovolval5lem2  47294  ovolval5lem3  47295  ovolval5  47296  ovnovollem2  47298  afv2eq12d  47876  uniimaelsetpreimafv  48069  fundcmpsurinjlem3  48073  imasetpreimafvbijlemfo  48078  fundcmpsurbijinjpreimafv  48080  dftpos5  49572  tposideq  49586  restcls2lem  49611  mreclat  49695  toplatglb  49699  swapf1a  49967  swapf2a  49969  swapf1  49970  swapf2  49972  setrecseq  50383