Theorem unieqi 4103

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

Syntax hints:   = wceq 1369   U.cuni 4094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-rex 2724  df-uni 4095

This theorem is referenced by:  elunirab  4106  unisn  4109  unidif0  4468  univ  4546  uniop  4597  unisuc  4798  dfiun3g  5095  op1sta  5324  op2nda  5327  dfdm2  5372  unixpid  5375  iotajust  5383  dfiota2  5385  cbviota  5389  sb8iota  5391  dffv4  5691  funfv2f  5763  funiunfv  5968  elunirnALT  5972  riotauni  6061  ordunisuc  6446  1st0  6586  2nd0  6587  unielxp  6615  brtpos0  6755  recsfval  6843  tz7.44-3  6867  uniqs  7163  xpassen  7408  dffi3  7684  dfsup2  7695  dfsup2OLD  7696  dfsup3OLD  7697  r1limg  7981  jech9.3  8024  rankxplim2  8090  rankxplim3  8091  rankxpsuc  8092  dfac5lem2  8297  kmlem11  8332  cflim2  8435  fin23lem30  8514  fin23lem34  8518  itunisuc  8591  itunitc  8593  ituniiun  8594  ac6num  8651  rankcf  8947  dprd2da  16544  dmdprdsplit2lem  16547  lssuni  17024  basdif0  18561  tgdif0  18600  neiptopuni  18737  restcls  18788  restntr  18789  pnrmopn  18950  cncmp  18998  discmp  19004  hauscmplem  19012  xkouni  19175  uptx  19201  ufildr  19507  ptcmplem3  19629  utop2nei  19828  utopreg  19830  zcld  20393  icccmp  20405  cncfcnvcn  20500  cnmpt2pc  20503  cnheibor  20530  evth  20534  evth2  20535  iunmbl  21037  voliun  21038  dvcnvrelem2  21493  ftc1  21517  aannenlem2  21798  tpr2rico  26345  cbvesum  26500  unibrsiga  26603  sxbrsigalem3  26690  dya2iocucvr  26702  sxbrsigalem1  26703  sibf0  26723  sibff  26725  sibfof  26729  sitgclg  26731  probfinmeasbOLD  26814  coinflipuniv  26867  cvmliftlem10  27186  dfon2lem7  27605  dfrdg2  27612  frrlem11  27783  dfiota3  27957  dffv5  27958  dfrdg4  27984  ordcmp  28296  ftc1cnnc  28469  refsum2cnlem1  29762  stoweidlem62  29860