Theorem unieqi 3819

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

Syntax hints:   = wceq 1353   U.cuni 3809

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3810

This theorem is referenced by:  elunirab  3822  unisn  3825  uniop  4255  unisuc  4413  unisucg  4414  univ  4476  dfiun3g  4884  op1sta  5110  op2nda  5113  dfdm2  5163  iotajust  5177  dfiota2  5179  cbviota  5183  sb8iota  5185  dffv4g  5512  funfvdm2f  5581  riotauni  5836  1st0  6144  2nd0  6145  unielxp  6174  brtpos0  6252  recsfval  6315  uniqs  6592  xpassen  6829  sup00  7001  suplocexprlemell  7711  uptx  13667