Theorem unieqi 3782

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

Syntax hints:   = wceq 1335   U.cuni 3772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rex 2441  df-uni 3773

This theorem is referenced by:  elunirab  3785  unisn  3788  uniop  4215  unisuc  4373  unisucg  4374  univ  4435  dfiun3g  4842  op1sta  5066  op2nda  5069  dfdm2  5119  iotajust  5133  dfiota2  5135  cbviota  5139  sb8iota  5141  dffv4g  5464  funfvdm2f  5532  riotauni  5783  1st0  6089  2nd0  6090  unielxp  6119  brtpos0  6196  recsfval  6259  uniqs  6535  xpassen  6772  sup00  6943  suplocexprlemell  7627  uptx  12645