Theorem uneq1i 3763

Description: Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
uneq1i.1	|- A = B

Assertion

Ref	Expression
uneq1i	|- ( A u. C ) = ( B u. C )

Proof of Theorem uneq1i

Step	Hyp	Ref	Expression
1		uneq1i.1	. 2 |- A = B
2		uneq1 3760	. 2 |- ( A = B -> ( A u. C ) = ( B u. C ) )
3	1, 2	ax-mp 5	1 |- ( A u. C ) = ( B u. C )

Syntax hints:   = wceq 1483   u. cun 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579

This theorem is referenced by:  un12  3771  unundi  3774  undif1  4043  dfif5  4102  tpcoma  4285  qdass  4288  qdassr  4289  tpidm12  4290  symdifv  4598  unidif0  4838  difxp2  5560  resasplit  6074  fresaun  6075  fresaunres2  6076  df2o3  7573  sbthlem6  8075  fodomr  8111  domss2  8119  domunfican  8233  kmlem11  8982  hashfun  13224  prmreclem2  15621  setscom  15903  gsummptfzsplitl  18333  uniioombllem3  23353  lhop  23779  ex-un  27281  ex-pw  27286  indifundif  29356  bnj1415  31106  subfacp1lem1  31161  dftrpred4g  31734  lineunray  32254  bj-2upln1upl  33012  poimirlem3  33412  poimirlem4  33413  poimirlem5  33414  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  dfrcl2  37966  iunrelexp0  37994  trclfvdecomr  38020  corcltrcl  38031  cotrclrcl  38034  df3o2  38322  fourierdlem80  40403  caragenuncllem  40726  carageniuncllem1  40735  1fzopredsuc  41334  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  lmod1  42281