Theorem unieqi 4920

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

Syntax hints:   = wceq 1542  ∪ cuni 4907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3954  df-ss 3964  df-uni 4908

This theorem is referenced by:  elunirab  4923  unisng  4928  unidif0  5357  univ  5450  uniop  5514  dfiun3g  5961  op1sta  6221  op2nda  6224  dfdm2  6277  unixpid  6280  unisucs  6438  iotajust  6491  dfiota2  6493  cbviotaw  6499  cbviotavw  6500  cbviota  6502  sb8iota  6504  dffv4  6885  funfv2f  6976  funiunfv  7242  elunirnALT  7246  riotauni  7366  ordunisuc  7815  1st0  7976  2nd0  7977  unielxp  8008  brtpos0  8213  frrlem5  8270  frrlem8  8273  frrlem10  8275  dfwrecsOLD  8293  dfrecs3  8367  dfrecs3OLD  8368  recsfval  8376  tz7.44-3  8403  nlim1  8484  nlim2  8485  uniqs  8767  xpassen  9062  dffi3  9422  dfsup2  9435  sup00  9455  r1limg  9762  jech9.3  9805  rankxplim2  9871  rankxplim3  9872  rankxpsuc  9873  dfac5lem2  10115  kmlem11  10151  cflim2  10254  fin23lem30  10333  fin23lem34  10337  itunisuc  10410  itunitc  10412  ituniiun  10413  ac6num  10470  rankcf  10768  dprd2da  19904  dmdprdsplit2lem  19907  lssuni  20538  basdif0  22438  tgdif0  22477  neiptopuni  22616  restcls  22667  restntr  22668  pnrmopn  22829  cncmp  22878  discmp  22884  hauscmplem  22892  unisngl  23013  xkouni  23085  uptx  23111  ufildr  23417  ptcmplem3  23540  utop2nei  23737  utopreg  23739  zcld  24311  icccmp  24323  cncfcnvcn  24423  cnmpopc  24426  cnheibor  24453  evth  24457  evth2  24458  iunmbl  25052  voliun  25053  dvcnvrelem2  25517  ftc1  25541  aannenlem2  25824  bday1s  27312  old0  27334  made0  27348  old1  27350  madeoldsuc  27359  circtopn  32755  locfinref  32759  zarmxt1  32798  tpr2rico  32830  cbvesum  32978  unibrsiga  33122  sxbrsigalem3  33209  dya2iocucvr  33221  sxbrsigalem1  33222  sibf0  33271  sibff  33273  sitgclg  33279  probfinmeasbALTV  33366  coinflipuniv  33418  cvmliftlem10  34223  dfon2lem7  34699  dfrdg2  34705  dfiota3  34833  dffv5  34834  dfrecs2  34860  dfrdg4  34861  ordcmp  35270  bj-nuliotaALT  35877  mptsnun  36158  finxp1o  36211  ftc1cnnc  36498  uniqsALTV  37136  cnvepima  37144  sn-iotalemcor  40987  onsucunitp  42056  dfom6  42215  refsum2cnlem1  43654  lptre2pt  44291  limclner  44302  limclr  44306  stoweidlem62  44713  fourierdlem42  44800  fourierdlem80  44837  fouriercnp  44877  qndenserrn  44950  salexct3  44993  salgencntex  44994  salgensscntex  44995  subsalsal  45010  0ome  45180  borelmbl  45287  mbfresmf  45390  cnfsmf  45391  incsmf  45393  smfmbfcex  45411  decsmf  45418  smfpimbor1lem2  45450  ipoglb0  47521  setrec2  47642