Theorem unieqi 4221

Description: Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
unieqi.1	|- A = B

Assertion

Ref	Expression
unieqi	|- U. A = U. B

Proof of Theorem unieqi

Step	Hyp	Ref	Expression
1		unieqi.1	. 2 |- A = B
2		unieq 4220	. 2 |- ( A = B -> U. A = U. B )
3	1, 2	ax-mp 5	1 |- U. A = U. B

Syntax hints:   = wceq 1455   U.cuni 4212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rex 2755  df-uni 4213

This theorem is referenced by:  elunirab  4224  unisn  4227  unidif0  4590  univ  4665  uniop  4718  dfiun3g  5106  op1sta  5337  op2nda  5340  dfdm2  5387  unixpid  5390  unisuc  5518  iotajust  5564  dfiota2  5566  cbviota  5570  sb8iota  5572  dffv4  5885  funfv2f  5957  funiunfv  6178  elunirnALT  6182  riotauni  6283  ordunisuc  6686  1st0  6826  2nd0  6827  unielxp  6856  brtpos0  7006  dfrecs3  7117  recsfval  7125  tz7.44-3  7152  uniqs  7449  xpassen  7692  dffi3  7971  dfsup2  7984  sup00  8004  r1limg  8268  jech9.3  8311  rankxplim2  8377  rankxplim3  8378  rankxpsuc  8379  dfac5lem2  8581  kmlem11  8616  cflim2  8719  fin23lem30  8798  fin23lem34  8802  itunisuc  8875  itunitc  8877  ituniiun  8878  ac6num  8935  rankcf  9228  dprd2da  17724  dmdprdsplit2lem  17727  lssuni  18212  basdif0  20017  tgdif0  20057  neiptopuni  20195  restcls  20246  restntr  20247  pnrmopn  20408  cncmp  20456  discmp  20462  hauscmplem  20470  unisngl  20591  xkouni  20663  uptx  20689  ufildr  20995  ptcmplem3  21118  utop2nei  21314  utopreg  21316  zcld  21880  icccmp  21892  cncfcnvcn  22002  cnmpt2pc  22005  cnheibor  22032  evth  22036  evth2  22037  iunmbl  22555  voliun  22556  dvcnvrelem2  23019  ftc1  23043  aannenlem2  23334  circtopn  28713  locfinref  28717  tpr2rico  28767  cbvesum  28912  unibrsiga  29057  sxbrsigalem3  29143  dya2iocucvr  29155  sxbrsigalem1  29156  sibf0  29216  sibff  29218  sitgclg  29224  probfinmeasbOLD  29310  coinflipuniv  29363  cvmliftlem10  30066  dfon2lem7  30484  dfrdg2  30491  frrlem11  30575  dfiota3  30739  dffv5  30740  dfrecs2  30766  dfrdg4  30767  ordcmp  31156  bj-nuliotaALT  31669  mptsnun  31786  finxp1o  31829  ftc1cnnc  32061  refsum2cnlem1  37398  lptre2pt  37758  limclner  37770  limclr  37774  stoweidlem62  37961  stoweidlem62OLD  37962  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem80  38088  fouriercnp  38128  qndenserrn  38206  salexct3  38239  salgencntex  38240  salgensscntex  38241  0ome  38388  borelmbl  38496