Theorem unieqi 4862

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 4861	. 2 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ∪ 𝐴 = ∪ 𝐵

Syntax hints:   = wceq 1542  ∪ cuni 4850

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-uni 4851

This theorem is referenced by:  elunirab  4865  unisng  4868  unidif0  5301  unidif0OLD  5302  univ  5403  uniop  5469  dfiun3g  5923  op1sta  6189  op2nda  6192  dfdm2  6245  unixpid  6248  unisucs  6402  iotajust  6453  dfiota2  6455  cbviotaw  6461  cbviotavw  6462  cbviota  6463  sb8iota  6465  dffv4  6837  funfv2f  6929  funiunfv  7203  elunirnALT  7207  riotauni  7330  ordunisuc  7783  1st0  7948  2nd0  7949  unielxp  7980  brtpos0  8183  frrlem5  8240  frrlem8  8243  frrlem10  8245  dfrecs3  8312  recsfval  8320  tz7.44-3  8347  nlim1  8424  nlim2  8425  uniqs  8720  xpassen  9009  dffi3  9344  dfsup2  9357  sup00  9378  r1limg  9695  jech9.3  9738  rankxplim2  9804  rankxplim3  9805  rankxpsuc  9806  dfac5lem2  10046  kmlem11  10083  cflim2  10185  fin23lem30  10264  fin23lem34  10268  itunisuc  10341  itunitc  10343  ituniiun  10344  ac6num  10401  rankcf  10700  dprd2da  20019  dmdprdsplit2lem  20022  lssuni  20934  basdif0  22918  tgdif0  22957  neiptopuni  23095  restcls  23146  restntr  23147  pnrmopn  23308  cncmp  23357  discmp  23363  hauscmplem  23371  unisngl  23492  xkouni  23564  uptx  23590  ufildr  23896  ptcmplem3  24019  utop2nei  24215  utopreg  24217  zcld  24779  icccmp  24791  cncfcnvcn  24892  cnmpopc  24895  cnheibor  24922  evth  24926  evth2  24927  iunmbl  25520  voliun  25521  dvcnvrelem2  25985  ftc1  26009  aannenlem2  26295  bday1  27806  old0  27831  made0  27855  old1  27857  madeoldsuc  27877  isconstr  33880  circtopn  33981  locfinref  33985  zarmxt1  34024  tpr2rico  34056  cbvesum  34186  cbvesumv  34187  unibrsiga  34330  sxbrsigalem3  34416  dya2iocucvr  34428  sxbrsigalem1  34429  sibf0  34478  sibff  34480  sitgclg  34486  probfinmeasbALTV  34573  coinflipuniv  34626  fineqvnttrclse  35268  wevgblacfn  35291  cvmliftlem10  35476  dfon2lem7  35969  dfrdg2  35975  dfiota3  36103  dffv5  36104  dfrecs2  36132  dfrdg4  36133  ordcmp  36629  ttcuni  36695  bj-nuliotaALT  37365  mptsnun  37655  finxp1o  37708  ftc1cnnc  38013  cnvepima  38658  sn-iotalemcor  42663  onsucunitp  43801  dfom6  43958  refsum2cnlem1  45468  lptre2pt  46068  limclner  46079  limclr  46083  stoweidlem62  46490  fourierdlem42  46577  fourierdlem80  46614  fouriercnp  46654  qndenserrn  46727  salexct3  46770  salgencntex  46771  salgensscntex  46772  subsalsal  46787  0ome  46957  borelmbl  47064  mbfresmf  47167  cnfsmf  47168  incsmf  47170  smfmbfcex  47188  decsmf  47195  smfpimbor1lem2  47227  dftpos5  49349  ipoglb0  49469  setrec2  50170