Theorem unieqi 4477

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

Syntax hints:   = wceq 1523  ∪ cuni 4468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-uni 4469

This theorem is referenced by:  elunirab  4480  unisn  4483  unidif0  4868  univ  4949  uniop  5006  dfiun3g  5410  op1sta  5654  op2nda  5658  dfdm2  5705  unixpid  5708  unisuc  5839  iotajust  5888  dfiota2  5890  cbviota  5894  sb8iota  5896  dffv4  6226  funfv2f  6306  funiunfv  6546  elunirnALT  6550  riotauni  6657  ordunisuc  7074  1st0  7216  2nd0  7217  unielxp  7248  brtpos0  7404  dfrecs3  7514  recsfval  7522  tz7.44-3  7549  uniqs  7850  xpassen  8095  dffi3  8378  dfsup2  8391  sup00  8411  r1limg  8672  jech9.3  8715  rankxplim2  8781  rankxplim3  8782  rankxpsuc  8783  dfac5lem2  8985  kmlem11  9020  cflim2  9123  fin23lem30  9202  fin23lem34  9206  itunisuc  9279  itunitc  9281  ituniiun  9282  ac6num  9339  rankcf  9637  dprd2da  18487  dmdprdsplit2lem  18490  lssuni  18988  basdif0  20805  tgdif0  20844  neiptopuni  20982  restcls  21033  restntr  21034  pnrmopn  21195  cncmp  21243  discmp  21249  hauscmplem  21257  unisngl  21378  xkouni  21450  uptx  21476  ufildr  21782  ptcmplem3  21905  utop2nei  22101  utopreg  22103  zcld  22663  icccmp  22675  cncfcnvcn  22771  cnmpt2pc  22774  cnheibor  22801  evth  22805  evth2  22806  iunmbl  23367  voliun  23368  dvcnvrelem2  23826  ftc1  23850  aannenlem2  24129  circtopn  30032  locfinref  30036  tpr2rico  30086  cbvesum  30232  unibrsiga  30377  sxbrsigalem3  30462  dya2iocucvr  30474  sxbrsigalem1  30475  sibf0  30524  sibff  30526  sitgclg  30532  probfinmeasbOLD  30618  coinflipuniv  30671  cvmliftlem10  31402  dfon2lem7  31818  dfrdg2  31825  frrlem6  31914  frrlem7  31915  frrlem10  31916  frrlem11  31917  noetalem4  31991  dfiota3  32155  dffv5  32156  dfrecs2  32182  dfrdg4  32183  ordcmp  32571  bj-nuliotaALT  33145  mptsnun  33316  finxp1o  33359  ftc1cnnc  33614  uniqsALTV  34242  refsum2cnlem1  39510  lptre2pt  40190  limclner  40201  limclr  40205  stoweidlem62  40597  fourierdlem42  40684  fourierdlem80  40721  fouriercnp  40761  qndenserrn  40837  salexct3  40878  salgencntex  40879  salgensscntex  40880  subsalsal  40895  0ome  41064  borelmbl  41171  mbfresmf  41269  cnfsmf  41270  incsmf  41272  smfmbfcex  41289  decsmf  41296  smfpimbor1lem2  41327  setrec2  42767