Theorem unieqi 3929

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

Syntax hints:   = wceq 1398   U.cuni 3919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-uni 3920

This theorem is referenced by:  elunirab  3932  unisn  3935  uniop  4377  unisuc  4539  unisucg  4540  univ  4602  dfiun3g  5019  op1sta  5249  op2nda  5252  dfdm2  5302  iotajust  5316  dfiota2  5318  cbviota  5322  cbviotavw  5323  sb8iota  5325  dffv4g  5672  funfvdm2f  5747  riotauni  6018  1st0  6351  2nd0  6352  unielxp  6381  brtpos0  6496  recsfval  6559  uniqs  6840  xpassen  7094  sup00  7307  suplocexprlemell  8044  uptx  15251