Theorem unieqi 4879

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

This proof depends on syntax axioms:   = wceq 1570  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868

This theorem is used by:  elunirab  4882  unisng  4885  unidif0  5321  unidif0OLD  5322  univ  5419  uniop  5485  dfiun3g  5947  op1sta  6216  op2nda  6219  dfdm2  6274  unixpid  6277  unisucs  6432  iotajust  6483  dfiota2  6485  cbviotaw  6491  cbviotavw  6492  cbviota  6493  sb8iota  6495  dffv4  6871  funfv2f  6963  funiunfv  7241  elunirnALT  7245  riotauni  7372  ordunisuc  7827  1st0  7991  2nd0  7992  unielxp  8023  brtpos0  8229  frrlem5  8287  frrlem8  8290  frrlem10  8292  dfrecs3  8359  recsfval  8367  tz7.44-3  8395  nlim1  8476  nlim2  8477  uniqs  8773  xpassen  9069  dffi3  9401  dfsup2  9414  sup00  9435  r1limg  9753  jech9.3  9796  rankxplim2  9866  rankxplim3  9867  rankxpsuc  9868  setrec2  9934  dfac5lem2  10160  kmlem11  10196  cflim2  10298  fin23lem30  10377  fin23lem34  10381  itunisuc  10454  itunitc  10456  ituniiun  10457  ac6num  10514  rankcf  10819  dprd2da  20205  dmdprdsplit2lem  20208  lssuni  21161  basdif0  23218  tgdif0  23257  neiptopuni  23395  restcls  23446  restntr  23447  pnrmopn  23608  cncmp  23657  discmp  23663  hauscmplem  23671  unisngl  23793  xkouni  23865  uptx  23891  ufildr  24197  ptcmplem3  24320  utop2nei  24516  utopreg  24518  zcld  25080  icccmp  25092  cncfcnvcn  25193  cnmpopc  25196  cnheibor  25223  evth  25227  evth2  25228  iunmbl  25821  voliun  25822  dvcnvrelem2  26285  ftc1  26309  aannenlem2  26605  bday1  28119  old0  28144  made0  28168  old1  28170  madeoldsuc  28190  isconstr  34287  circtopn  34388  locfinref  34392  zarmxt1  34431  tpr2rico  34463  cbvesum  34593  cbvesumv  34594  unibrsiga  34738  sxbrsigalem3  34824  dya2iocucvr  34836  sxbrsigalem1  34837  sibf0  34886  sibff  34888  sitgclg  34894  probfinmeasbALTV  34981  coinflipuniv  35034  fineqvnttrclse  35711  wevgblacfn  35809  cvmliftlem10  35974  dfon2lem7  36467  dfrdg2  36473  dfiota3  36601  dffv5  36602  dfrecs2  36630  dfrdg4  36631  ordcmp  37151  ttcuni  37217  bj-nuliotaALT  37887  mptsnun  38176  finxp1o  38229  ftc1cnnc  38524  cnvepima  39183  sn-iotalemcor  43190  onsucunitp  44312  dfom6  44469  refsum2cnlem1  45969  lptre2pt  46566  limclner  46577  limclr  46581  stoweidlem62  46988  fourierdlem42  47075  fourierdlem80  47112  fouriercnp  47152  qndenserrn  47225  salexct3  47268  salgencntex  47269  salgensscntex  47270  subsalsal  47285  0ome  47455  borelmbl  47562  mbfresmf  47665  cnfsmf  47666  incsmf  47668  smfmbfcex  47686  decsmf  47693  smfpimbor1lem2  47725  dftpos5  49898  ipoglb0  50018