Theorem uneq1i 4137

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

Hypothesis

Ref	Expression
uneq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
uneq1i	⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)

Proof of Theorem uneq1i

Step	Hyp	Ref	Expression
1		uneq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		uneq1 4134	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)

Syntax hints:   = wceq 1537   ∪ cun 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943

This theorem is referenced by:  un12  4145  unundi  4148  undif1  4426  dfif5  4485  tpcoma  4688  qdass  4691  qdassr  4692  tpidm12  4693  symdifv  5010  unidif0  5262  difxp2  6025  resasplit  6550  fresaun  6551  fresaunres2  6552  df2o3  8119  sbthlem6  8634  fodomr  8670  domss2  8678  domunfican  8793  kmlem11  9588  hashfun  13801  prmreclem2  16255  setscom  16529  gsummptfzsplitl  19055  uniioombllem3  24188  lhop  24615  ex-un  28205  ex-pw  28210  indifundif  30287  cycpmrn  30787  bnj1415  32312  subfacp1lem1  32428  dftrpred4g  33075  lineunray  33610  bj-2upln1upl  34338  poimirlem3  34897  poimirlem4  34898  poimirlem5  34899  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem22  34916  dfrcl2  40026  iunrelexp0  40054  trclfvdecomr  40080  corcltrcl  40091  cotrclrcl  40094  df3o2  40381  fourierdlem80  42478  caragenuncllem  42801  carageniuncllem1  42810  1fzopredsuc  43531  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  lmod1  44554