Theorem unieqi 3902

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

Syntax hints:   = wceq 1397   U.cuni 3892

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-rex 2515  df-uni 3893

This theorem is referenced by:  elunirab  3905  unisn  3908  uniop  4347  unisuc  4509  unisucg  4510  univ  4572  dfiun3g  4988  op1sta  5217  op2nda  5220  dfdm2  5270  iotajust  5284  dfiota2  5286  cbviota  5290  cbviotavw  5291  sb8iota  5293  dffv4g  5636  funfvdm2f  5711  riotauni  5980  1st0  6309  2nd0  6310  unielxp  6339  brtpos0  6420  recsfval  6483  uniqs  6764  xpassen  7016  sup00  7204  suplocexprlemell  7935  uptx  15024