Theorem unieqi 4097

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

Syntax hints:   = wceq 1364   U.cuni 4088

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 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rex 2719  df-uni 4089

This theorem is referenced by:  elunirab  4100  unisn  4103  unidif0  4462  univ  4540  uniop  4591  unisuc  4791  dfiun3g  5088  op1sta  5318  op2nda  5321  dfdm2  5366  unixpid  5369  iotajust  5377  dfiota2  5379  cbviota  5383  sb8iota  5385  dffv4  5685  funfv2f  5757  funiunfv  5962  elunirnALT  5966  riotauni  6056  ordunisuc  6442  1st0  6582  2nd0  6583  unielxp  6611  brtpos0  6751  recsfval  6836  tz7.44-3  6860  uniqs  7156  xpassen  7401  dffi3  7677  dfsup2  7688  dfsup2OLD  7689  dfsup3OLD  7690  r1limg  7974  jech9.3  8017  rankxplim2  8083  rankxplim3  8084  rankxpsuc  8085  dfac5lem2  8290  kmlem11  8325  cflim2  8428  fin23lem30  8507  fin23lem34  8511  itunisuc  8584  itunitc  8586  ituniiun  8587  ac6num  8644  rankcf  8940  dprd2da  16531  dmdprdsplit2lem  16534  lssuni  16999  basdif0  18517  tgdif0  18556  neiptopuni  18693  restcls  18744  restntr  18745  pnrmopn  18906  cncmp  18954  discmp  18960  hauscmplem  18968  xkouni  19131  uptx  19157  ufildr  19463  ptcmplem3  19585  utop2nei  19784  utopreg  19786  zcld  20349  icccmp  20361  cncfcnvcn  20456  cnmpt2pc  20459  cnheibor  20486  evth  20490  evth2  20491  iunmbl  20993  voliun  20994  dvcnvrelem2  21449  ftc1  21473  aannenlem2  21754  tpr2rico  26278  cbvesum  26433  unibrsiga  26536  sxbrsigalem3  26623  dya2iocucvr  26635  sxbrsigalem1  26636  sibf0  26650  sibff  26652  sibfof  26656  sitgclg  26658  probfinmeasbOLD  26741  coinflipuniv  26794  cvmliftlem10  27113  dfon2lem7  27531  dfrdg2  27538  frrlem11  27709  dfiota3  27883  dffv5  27884  dfrdg4  27910  ordcmp  28223  ftc1cnnc  28391  refsum2cnlem1  29684  stoweidlem62  29782