Theorem unieqi 4247

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

Syntax hints:   = wceq 1374   U.cuni 4238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rex 2813  df-uni 4239

This theorem is referenced by:  elunirab  4250  unisn  4253  unidif0  4613  univ  4691  uniop  4743  unisuc  4947  dfiun3g  5246  op1sta  5481  op2nda  5484  dfdm2  5530  unixpid  5533  iotajust  5541  dfiota2  5543  cbviota  5547  sb8iota  5549  dffv4  5854  funfv2f  5927  funiunfv  6139  elunirnALT  6143  riotauni  6242  ordunisuc  6638  1st0  6780  2nd0  6781  unielxp  6810  brtpos0  6952  recsfval  7040  tz7.44-3  7064  uniqs  7361  xpassen  7601  dffi3  7880  dfsup2  7891  dfsup2OLD  7892  dfsup3OLD  7893  r1limg  8178  jech9.3  8221  rankxplim2  8287  rankxplim3  8288  rankxpsuc  8289  dfac5lem2  8494  kmlem11  8529  cflim2  8632  fin23lem30  8711  fin23lem34  8715  itunisuc  8788  itunitc  8790  ituniiun  8791  ac6num  8848  rankcf  9144  dprd2da  16874  dmdprdsplit2lem  16877  lssuni  17362  basdif0  19214  tgdif0  19253  neiptopuni  19390  restcls  19441  restntr  19442  pnrmopn  19603  cncmp  19651  discmp  19657  hauscmplem  19665  xkouni  19828  uptx  19854  ufildr  20160  ptcmplem3  20282  utop2nei  20481  utopreg  20483  zcld  21046  icccmp  21058  cncfcnvcn  21153  cnmpt2pc  21156  cnheibor  21183  evth  21187  evth2  21188  iunmbl  21691  voliun  21692  dvcnvrelem2  22147  ftc1  22171  aannenlem2  22452  tpr2rico  27516  circtopn  27624  cbvesum  27680  unibrsiga  27783  sxbrsigalem3  27869  dya2iocucvr  27881  sxbrsigalem1  27882  sibf0  27902  sibff  27904  sibfof  27908  sitgclg  27910  probfinmeasbOLD  27993  coinflipuniv  28046  cvmliftlem10  28365  dfon2lem7  28784  dfrdg2  28791  frrlem11  28962  dfiota3  29136  dffv5  29137  dfrdg4  29163  ordcmp  29475  ftc1cnnc  29653  refsum2cnlem1  30945  lptre2pt  31137  limclner  31148  limclr  31152  stoweidlem62  31317  fourierdlem42  31404  fourierdlem80  31442  fouriercnp  31482  bj-nuliotaALT  33543