Theorem unieqi 4225

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 4224	. 2 |- ( A = B -> U. A = U. B )
3	1, 2	ax-mp 5	1 |- U. A = U. B

Syntax hints:   = wceq 1437   U.cuni 4216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-rex 2781  df-uni 4217

This theorem is referenced by:  elunirab  4228  unisn  4231  unidif0  4593  univ  4668  uniop  4719  dfiun3g  5102  op1sta  5333  op2nda  5336  dfdm2  5383  unixpid  5386  unisuc  5514  iotajust  5560  dfiota2  5562  cbviota  5566  sb8iota  5568  dffv4  5874  funfv2f  5946  funiunfv  6164  elunirnALT  6168  riotauni  6269  ordunisuc  6669  1st0  6809  2nd0  6810  unielxp  6839  brtpos0  6984  dfrecs3  7095  recsfval  7103  tz7.44-3  7130  uniqs  7427  xpassen  7668  dffi3  7947  dfsup2  7960  sup00  7980  r1limg  8243  jech9.3  8286  rankxplim2  8352  rankxplim3  8353  rankxpsuc  8354  dfac5lem2  8555  kmlem11  8590  cflim2  8693  fin23lem30  8772  fin23lem34  8776  itunisuc  8849  itunitc  8851  ituniiun  8852  ac6num  8909  rankcf  9202  dprd2da  17662  dmdprdsplit2lem  17665  lssuni  18150  basdif0  19954  tgdif0  19994  neiptopuni  20132  restcls  20183  restntr  20184  pnrmopn  20345  cncmp  20393  discmp  20399  hauscmplem  20407  unisngl  20528  xkouni  20600  uptx  20626  ufildr  20932  ptcmplem3  21055  utop2nei  21251  utopreg  21253  zcld  21817  icccmp  21829  cncfcnvcn  21939  cnmpt2pc  21942  cnheibor  21969  evth  21973  evth2  21974  iunmbl  22492  voliun  22493  dvcnvrelem2  22956  ftc1  22980  aannenlem2  23271  circtopn  28659  locfinref  28663  tpr2rico  28713  cbvesum  28858  unibrsiga  29003  sxbrsigalem3  29089  dya2iocucvr  29101  sxbrsigalem1  29102  sibf0  29162  sibff  29164  sitgclg  29170  probfinmeasbOLD  29256  coinflipuniv  29309  cvmliftlem10  30012  dfon2lem7  30429  dfrdg2  30436  frrlem11  30520  dfiota3  30682  dffv5  30683  dfrecs2  30709  dfrdg4  30710  ordcmp  31099  bj-nuliotaALT  31578  mptsnun  31681  ftc1cnnc  31929  refsum2cnlem1  37218  lptre2pt  37539  limclner  37551  limclr  37555  stoweidlem62  37742  stoweidlem62OLD  37743  fourierdlem42  37831  fourierdlem42OLD  37832  fourierdlem80  37869  fouriercnp  37909  0ome  38128