Theorem unieqi 4243

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

Syntax hints:   = wceq 1383   U.cuni 4234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-uni 4235

This theorem is referenced by:  elunirab  4246  unisn  4249  unidif0  4610  univ  4688  uniop  4740  unisuc  4944  dfiun3g  5245  op1sta  5480  op2nda  5483  dfdm2  5529  unixpid  5532  iotajust  5540  dfiota2  5542  cbviota  5546  sb8iota  5548  dffv4  5853  funfv2f  5927  funiunfv  6145  elunirnALT  6149  riotauni  6248  ordunisuc  6652  1st0  6791  2nd0  6792  unielxp  6821  brtpos0  6964  recsfval  7052  tz7.44-3  7076  uniqs  7373  xpassen  7613  dffi3  7893  dfsup2  7904  dfsup2OLD  7905  dfsup3OLD  7906  r1limg  8192  jech9.3  8235  rankxplim2  8301  rankxplim3  8302  rankxpsuc  8303  dfac5lem2  8508  kmlem11  8543  cflim2  8646  fin23lem30  8725  fin23lem34  8729  itunisuc  8802  itunitc  8804  ituniiun  8805  ac6num  8862  rankcf  9158  dprd2da  16965  dmdprdsplit2lem  16968  lssuni  17460  basdif0  19327  tgdif0  19367  neiptopuni  19504  restcls  19555  restntr  19556  pnrmopn  19717  cncmp  19765  discmp  19771  hauscmplem  19779  unisngl  19901  xkouni  19973  uptx  19999  ufildr  20305  ptcmplem3  20427  utop2nei  20626  utopreg  20628  zcld  21191  icccmp  21203  cncfcnvcn  21298  cnmpt2pc  21301  cnheibor  21328  evth  21332  evth2  21333  iunmbl  21836  voliun  21837  dvcnvrelem2  22292  ftc1  22316  aannenlem2  22597  circtopn  27713  locfinref  27717  tpr2rico  27767  cbvesum  27927  unibrsiga  28030  sxbrsigalem3  28116  dya2iocucvr  28128  sxbrsigalem1  28129  sibf0  28149  sibff  28151  sitgclg  28157  probfinmeasbOLD  28240  coinflipuniv  28293  cvmliftlem10  28612  dfon2lem7  29196  dfrdg2  29203  frrlem11  29374  dfiota3  29548  dffv5  29549  dfrdg4  29575  ordcmp  29887  ftc1cnnc  30064  refsum2cnlem1  31366  lptre2pt  31554  limclner  31565  limclr  31569  stoweidlem62  31733  fourierdlem42  31820  fourierdlem80  31858  fouriercnp  31898  bj-nuliotaALT  34329