Theorem unieqi 4877

Description: Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
unieqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
unieqi	⊢ ∪ 𝐴 = ∪ 𝐵

Proof of Theorem unieqi

Step	Hyp	Ref	Expression
1		unieqi.1	. 2 ⊢ 𝐴 = 𝐵
2		unieq 4876	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ∪ 𝐴 = ∪ 𝐵

Syntax hints:   = wceq 1542  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-uni 4866

This theorem is referenced by:  elunirab  4880  unisng  4883  unidif0  5309  univ  5408  uniop  5473  dfiun3g  5927  op1sta  6193  op2nda  6196  dfdm2  6249  unixpid  6252  unisucs  6406  iotajust  6457  dfiota2  6459  cbviotaw  6465  cbviotavw  6466  cbviota  6467  sb8iota  6469  dffv4  6841  funfv2f  6933  funiunfv  7206  elunirnALT  7210  riotauni  7333  ordunisuc  7786  1st0  7951  2nd0  7952  unielxp  7983  brtpos0  8187  frrlem5  8244  frrlem8  8247  frrlem10  8249  dfrecs3  8316  recsfval  8324  tz7.44-3  8351  nlim1  8428  nlim2  8429  uniqs  8724  xpassen  9013  dffi3  9348  dfsup2  9361  sup00  9382  r1limg  9697  jech9.3  9740  rankxplim2  9806  rankxplim3  9807  rankxpsuc  9808  dfac5lem2  10048  kmlem11  10085  cflim2  10187  fin23lem30  10266  fin23lem34  10270  itunisuc  10343  itunitc  10345  ituniiun  10346  ac6num  10403  rankcf  10702  dprd2da  19990  dmdprdsplit2lem  19993  lssuni  20907  basdif0  22914  tgdif0  22953  neiptopuni  23091  restcls  23142  restntr  23143  pnrmopn  23304  cncmp  23353  discmp  23359  hauscmplem  23367  unisngl  23488  xkouni  23560  uptx  23586  ufildr  23892  ptcmplem3  24015  utop2nei  24211  utopreg  24213  zcld  24775  icccmp  24787  cncfcnvcn  24892  cnmpopc  24895  cnheibor  24927  evth  24931  evth2  24932  iunmbl  25527  voliun  25528  dvcnvrelem2  25996  ftc1  26022  aannenlem2  26310  bday1  27827  old0  27852  made0  27876  old1  27878  madeoldsuc  27898  isconstr  33920  circtopn  34021  locfinref  34025  zarmxt1  34064  tpr2rico  34096  cbvesum  34226  cbvesumv  34227  unibrsiga  34370  sxbrsigalem3  34456  dya2iocucvr  34468  sxbrsigalem1  34469  sibf0  34518  sibff  34520  sitgclg  34526  probfinmeasbALTV  34613  coinflipuniv  34666  fineqvnttrclse  35308  wevgblacfn  35331  cvmliftlem10  35516  dfon2lem7  36009  dfrdg2  36015  dfiota3  36143  dffv5  36144  dfrecs2  36172  dfrdg4  36173  ordcmp  36669  bj-nuliotaALT  37333  mptsnun  37621  finxp1o  37674  ftc1cnnc  37972  cnvepima  38617  sn-iotalemcor  42623  onsucunitp  43759  dfom6  43916  refsum2cnlem1  45426  lptre2pt  46027  limclner  46038  limclr  46042  stoweidlem62  46449  fourierdlem42  46536  fourierdlem80  46573  fouriercnp  46613  qndenserrn  46686  salexct3  46729  salgencntex  46730  salgensscntex  46731  subsalsal  46746  0ome  46916  borelmbl  47023  mbfresmf  47126  cnfsmf  47127  incsmf  47129  smfmbfcex  47147  decsmf  47154  smfpimbor1lem2  47186  dftpos5  49262  ipoglb0  49382  setrec2  50083