Theorem unieqi 4868

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

Syntax hints:   = wceq 1541  ∪ cuni 4856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4857

This theorem is referenced by:  elunirab  4871  unisng  4874  unidif0  5296  univ  5390  uniop  5453  dfiun3g  5906  op1sta  6172  op2nda  6175  dfdm2  6228  unixpid  6231  unisucs  6385  iotajust  6436  dfiota2  6438  cbviotaw  6444  cbviotavw  6445  cbviota  6446  sb8iota  6448  dffv4  6819  funfv2f  6911  funiunfv  7182  elunirnALT  7186  riotauni  7309  ordunisuc  7762  1st0  7927  2nd0  7928  unielxp  7959  brtpos0  8163  frrlem5  8220  frrlem8  8223  frrlem10  8225  dfrecs3  8292  recsfval  8300  tz7.44-3  8327  nlim1  8404  nlim2  8405  uniqs  8698  xpassen  8984  dffi3  9315  dfsup2  9328  sup00  9349  r1limg  9664  jech9.3  9707  rankxplim2  9773  rankxplim3  9774  rankxpsuc  9775  dfac5lem2  10015  kmlem11  10052  cflim2  10154  fin23lem30  10233  fin23lem34  10237  itunisuc  10310  itunitc  10312  ituniiun  10313  ac6num  10370  rankcf  10668  dprd2da  19956  dmdprdsplit2lem  19959  lssuni  20872  basdif0  22868  tgdif0  22907  neiptopuni  23045  restcls  23096  restntr  23097  pnrmopn  23258  cncmp  23307  discmp  23313  hauscmplem  23321  unisngl  23442  xkouni  23514  uptx  23540  ufildr  23846  ptcmplem3  23969  utop2nei  24165  utopreg  24167  zcld  24729  icccmp  24741  cncfcnvcn  24846  cnmpopc  24849  cnheibor  24881  evth  24885  evth2  24886  iunmbl  25481  voliun  25482  dvcnvrelem2  25950  ftc1  25976  aannenlem2  26264  bday1s  27775  old0  27800  made0  27818  old1  27820  madeoldsuc  27830  zs12bday  28394  isconstr  33749  circtopn  33850  locfinref  33854  zarmxt1  33893  tpr2rico  33925  cbvesum  34055  cbvesumv  34056  unibrsiga  34199  sxbrsigalem3  34285  dya2iocucvr  34297  sxbrsigalem1  34298  sibf0  34347  sibff  34349  sitgclg  34355  probfinmeasbALTV  34442  coinflipuniv  34495  fineqvnttrclse  35144  wevgblacfn  35153  cvmliftlem10  35338  dfon2lem7  35831  dfrdg2  35837  dfiota3  35965  dffv5  35966  dfrecs2  35994  dfrdg4  35995  ordcmp  36491  bj-nuliotaALT  37102  mptsnun  37383  finxp1o  37436  ftc1cnnc  37731  cnvepima  38368  sn-iotalemcor  42314  onsucunitp  43465  dfom6  43623  refsum2cnlem1  45133  lptre2pt  45737  limclner  45748  limclr  45752  stoweidlem62  46159  fourierdlem42  46246  fourierdlem80  46283  fouriercnp  46323  qndenserrn  46396  salexct3  46439  salgencntex  46440  salgensscntex  46441  subsalsal  46456  0ome  46626  borelmbl  46733  mbfresmf  46836  cnfsmf  46837  incsmf  46839  smfmbfcex  46857  decsmf  46864  smfpimbor1lem2  46896  dftpos5  48973  ipoglb0  49093  setrec2  49795