Theorem unieqi 3877

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

Syntax hints:   = wceq 1375   U.cuni 3867

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-rex 2494  df-uni 3868

This theorem is referenced by:  elunirab  3880  unisn  3883  uniop  4321  unisuc  4481  unisucg  4482  univ  4544  dfiun3g  4957  op1sta  5186  op2nda  5189  dfdm2  5239  iotajust  5253  dfiota2  5255  cbviota  5259  cbviotavw  5260  sb8iota  5262  dffv4g  5600  funfvdm2f  5672  riotauni  5934  1st0  6260  2nd0  6261  unielxp  6290  brtpos0  6368  recsfval  6431  uniqs  6710  xpassen  6957  sup00  7138  suplocexprlemell  7868  uptx  14913