Theorem unieqi 4445

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

Syntax hints:   = wceq 1483  ∪ cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-uni 4437

This theorem is referenced by:  elunirab  4448  unisn  4451  unidif0  4838  univ  4919  uniop  4977  dfiun3g  5378  op1sta  5617  op2nda  5620  dfdm2  5667  unixpid  5670  unisuc  5801  iotajust  5850  dfiota2  5852  cbviota  5856  sb8iota  5858  dffv4  6188  funfv2f  6267  funiunfv  6506  elunirnALT  6510  riotauni  6617  ordunisuc  7032  1st0  7174  2nd0  7175  unielxp  7204  brtpos0  7359  dfrecs3  7469  recsfval  7477  tz7.44-3  7504  uniqs  7807  xpassen  8054  dffi3  8337  dfsup2  8350  sup00  8370  r1limg  8634  jech9.3  8677  rankxplim2  8743  rankxplim3  8744  rankxpsuc  8745  dfac5lem2  8947  kmlem11  8982  cflim2  9085  fin23lem30  9164  fin23lem34  9168  itunisuc  9241  itunitc  9243  ituniiun  9244  ac6num  9301  rankcf  9599  dprd2da  18441  dmdprdsplit2lem  18444  lssuni  18940  basdif0  20757  tgdif0  20796  neiptopuni  20934  restcls  20985  restntr  20986  pnrmopn  21147  cncmp  21195  discmp  21201  hauscmplem  21209  unisngl  21330  xkouni  21402  uptx  21428  ufildr  21735  ptcmplem3  21858  utop2nei  22054  utopreg  22056  zcld  22616  icccmp  22628  cncfcnvcn  22724  cnmpt2pc  22727  cnheibor  22754  evth  22758  evth2  22759  iunmbl  23321  voliun  23322  dvcnvrelem2  23781  ftc1  23805  aannenlem2  24084  circtopn  29904  locfinref  29908  tpr2rico  29958  cbvesum  30104  unibrsiga  30249  sxbrsigalem3  30334  dya2iocucvr  30346  sxbrsigalem1  30347  sibf0  30396  sibff  30398  sitgclg  30404  probfinmeasbOLD  30490  coinflipuniv  30543  cvmliftlem10  31276  dfon2lem7  31694  dfrdg2  31701  frrlem11  31792  noetalem4  31866  dfiota3  32030  dffv5  32031  dfrecs2  32057  dfrdg4  32058  ordcmp  32446  bj-nuliotaALT  33020  mptsnun  33186  finxp1o  33229  ftc1cnnc  33484  uniqsALTV  34101  refsum2cnlem1  39196  lptre2pt  39872  limclner  39883  limclr  39887  stoweidlem62  40279  fourierdlem42  40366  fourierdlem80  40403  fouriercnp  40443  qndenserrn  40519  salexct3  40560  salgencntex  40561  salgensscntex  40562  subsalsal  40577  0ome  40743  borelmbl  40850  mbfresmf  40948  cnfsmf  40949  incsmf  40951  smfmbfcex  40968  decsmf  40975  smfpimbor1lem2  41006  setrec2  42442