Theorem unieqi 4878

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

This proof depends on syntax axioms:   = wceq 1569  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867

This theorem is used by:  elunirab  4881  unisng  4884  unidif0  5320  unidif0OLD  5321  univ  5418  uniop  5487  dfiun3g  5949  op1sta  6226  op2nda  6229  dfdm2  6284  unixpid  6287  unisucs  6442  iotajust  6493  dfiota2  6495  cbviotaw  6501  cbviotavw  6502  cbviota  6503  sb8iota  6505  dffv4  6882  funfv2f  6974  funiunfv  7252  elunirnALT  7256  riotauni  7383  ordunisuc  7843  1st0  8007  2nd0  8008  unielxp  8039  brtpos0  8250  frrlem5  8308  frrlem8  8311  frrlem10  8313  dfrecs3  8380  recsfval  8388  tz7.44-3  8416  nlim1  8497  nlim2  8498  uniqs  8794  xpassen  9090  dffi3  9423  dfsup2  9436  sup00  9457  r1limg  9778  jech9.3OLD  9823  rankxplim2  9897  rankxplim3  9898  rankxpsuc  9899  setrec2  9977  dfac5lem2  10203  kmlem11  10239  cflim2  10341  fin23lem30  10420  fin23lem34  10424  itunisuc  10497  itunitc  10499  ituniiun  10500  ac6num  10557  rankcf  10862  dprd2da  20258  dmdprdsplit2lem  20261  lssuni  21214  basdif0  23271  tgdif0  23310  neiptopuni  23448  restcls  23499  restntr  23500  pnrmopn  23661  cncmp  23710  discmp  23716  hauscmplem  23724  unisngl  23846  xkouni  23918  uptx  23944  ufildr  24250  ptcmplem3  24373  utop2nei  24569  utopreg  24571  zcld  25133  icccmp  25145  cncfcnvcn  25246  cnmpopc  25249  cnheibor  25276  evth  25280  evth2  25281  iunmbl  25874  voliun  25875  dvcnvrelem2  26338  ftc1  26362  aannenlem2  26656  bday1  28200  old0  28225  made0  28249  old1  28251  madeoldsuc  28271  isconstr  34368  circtopn  34469  locfinref  34473  zarmxt1  34512  tpr2rico  34544  cbvesum  34674  cbvesumv  34675  unibrsiga  34819  sxbrsigalem3  34904  dya2iocucvr  34916  sxbrsigalem1  34917  sibf0  34966  sibff  34968  sitgclg  34974  probfinmeasbALTV  35061  coinflipuniv  35114  fineqvnttrclse  35792  wevgblacfn  35890  cvmliftlem10  36059  dfon2lem7  36551  dfrdg2  36557  dfiota3  36685  dffv5  36686  dfrecs2  36714  dfrdg4  36715  ordcmp  37235  ttcuni  37301  bj-nuliotaALT  37973  mptsnun  38263  finxp1o  38316  ftc1cnnc  38611  cnvepima  39270  sn-iotalemcor  43277  onsucunitp  44375  dfom6  44532  refsum2cnlem1  46054  lptre2pt  46650  limclner  46661  limclr  46665  stoweidlem62  47072  fourierdlem42  47159  fourierdlem80  47196  fouriercnp  47236  qndenserrn  47309  salexct3  47352  salgencntex  47353  salgensscntex  47354  subsalsal  47369  0ome  47539  borelmbl  47646  mbfresmf  47749  cnfsmf  47750  incsmf  47752  smfmbfcex  47770  decsmf  47777  smfpimbor1lem2  47809  dftpos5  49982  ipoglb0  50102