Theorem unieqi 4668

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

Syntax hints:   = wceq 1658  ∪ cuni 4659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-rex 3124  df-uni 4660

This theorem is referenced by:  elunirab  4671  unisng  4674  unisnOLD  4676  unidif0  5061  univ  5141  uniop  5202  dfiun3g  5612  op1sta  5860  op2nda  5863  dfdm2  5909  unixpid  5912  unisuc  6040  iotajust  6086  dfiota2  6088  cbviota  6092  sb8iota  6094  dffv4  6431  funfv2f  6515  funiunfv  6762  elunirnALT  6766  riotauni  6873  ordunisuc  7294  1st0  7435  2nd0  7436  unielxp  7467  brtpos0  7625  dfrecs3  7736  recsfval  7744  tz7.44-3  7771  uniqs  8073  xpassen  8324  dffi3  8607  dfsup2  8620  sup00  8640  r1limg  8912  jech9.3  8955  rankxplim2  9021  rankxplim3  9022  rankxpsuc  9023  dfac5lem2  9261  kmlem11  9298  cflim2  9401  fin23lem30  9480  fin23lem34  9484  itunisuc  9557  itunitc  9559  ituniiun  9560  ac6num  9617  rankcf  9915  dprd2da  18796  dmdprdsplit2lem  18799  lssuni  19297  basdif0  21129  tgdif0  21168  neiptopuni  21306  restcls  21357  restntr  21358  pnrmopn  21519  cncmp  21567  discmp  21573  hauscmplem  21581  unisngl  21702  xkouni  21774  uptx  21800  ufildr  22106  ptcmplem3  22229  utop2nei  22425  utopreg  22427  zcld  22987  icccmp  22999  cncfcnvcn  23095  cnmpt2pc  23098  cnheibor  23125  evth  23129  evth2  23130  iunmbl  23720  voliun  23721  dvcnvrelem2  24181  ftc1  24205  aannenlem2  24484  circtopn  30450  locfinref  30454  tpr2rico  30504  cbvesum  30650  unibrsiga  30795  sxbrsigalem3  30880  dya2iocucvr  30892  sxbrsigalem1  30893  sibf0  30942  sibff  30944  sitgclg  30950  probfinmeasbOLD  31037  coinflipuniv  31090  cvmliftlem10  31823  dfon2lem7  32233  dfrdg2  32240  frrlem6  32329  frrlem7  32330  frrlem10  32331  frrlem11  32332  noetalem4  32406  dfiota3  32570  dffv5  32571  dfrecs2  32597  dfrdg4  32598  ordcmp  32980  bj-nuliotaALT  33543  mptsnun  33733  finxp1o  33775  ftc1cnnc  34028  uniqsALTV  34650  refsum2cnlem1  40015  lptre2pt  40668  limclner  40679  limclr  40683  stoweidlem62  41074  fourierdlem42  41161  fourierdlem80  41198  fouriercnp  41238  qndenserrn  41311  salexct3  41352  salgencntex  41353  salgensscntex  41354  subsalsal  41369  0ome  41538  borelmbl  41645  mbfresmf  41743  cnfsmf  41744  incsmf  41746  smfmbfcex  41763  decsmf  41770  smfpimbor1lem2  41801  setrec2  43338