Theorem unieqi 4172

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

Syntax hints:   = wceq 1399   U.cuni 4163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rex 2738  df-uni 4164

This theorem is referenced by:  elunirab  4175  unisn  4178  unidif0  4538  univ  4613  uniop  4664  unisuc  4868  dfiun3g  5168  op1sta  5398  op2nda  5401  dfdm2  5448  unixpid  5451  iotajust  5459  dfiota2  5461  cbviota  5465  sb8iota  5467  dffv4  5771  funfv2f  5843  funiunfv  6061  elunirnALT  6065  riotauni  6164  ordunisuc  6566  1st0  6705  2nd0  6706  unielxp  6735  brtpos0  6880  recsfval  6968  tz7.44-3  6992  uniqs  7289  xpassen  7530  dffi3  7806  dfsup2  7817  dfsup2OLD  7818  r1limg  8102  jech9.3  8145  rankxplim2  8211  rankxplim3  8212  rankxpsuc  8213  dfac5lem2  8418  kmlem11  8453  cflim2  8556  fin23lem30  8635  fin23lem34  8639  itunisuc  8712  itunitc  8714  ituniiun  8715  ac6num  8772  rankcf  9066  dprd2da  17204  dmdprdsplit2lem  17207  lssuni  17699  basdif0  19539  tgdif0  19579  neiptopuni  19717  restcls  19768  restntr  19769  pnrmopn  19930  cncmp  19978  discmp  19984  hauscmplem  19992  unisngl  20113  xkouni  20185  uptx  20211  ufildr  20517  ptcmplem3  20639  utop2nei  20838  utopreg  20840  zcld  21403  icccmp  21415  cncfcnvcn  21510  cnmpt2pc  21513  cnheibor  21540  evth  21544  evth2  21545  iunmbl  22048  voliun  22049  dvcnvrelem2  22504  ftc1  22528  aannenlem2  22810  circtopn  27994  locfinref  27998  tpr2rico  28048  cbvesum  28190  unibrsiga  28313  sxbrsigalem3  28399  dya2iocucvr  28411  sxbrsigalem1  28412  sibf0  28459  sibff  28461  sitgclg  28467  probfinmeasbOLD  28550  coinflipuniv  28603  cvmliftlem10  28928  dfon2lem7  29386  dfrdg2  29393  frrlem11  29564  dfiota3  29726  dffv5  29727  dfrdg4  29753  ordcmp  30065  ftc1cnnc  30255  refsum2cnlem1  31579  lptre2pt  31812  limclner  31823  limclr  31827  stoweidlem62  32010  fourierdlem42  32097  fourierdlem80  32135  fouriercnp  32175  bj-nuliotaALT  34935