Theorem uneq1i 4098

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 4095	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)

Syntax hints:   = wceq 1542   ∪ cun 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-un 3897

This theorem is referenced by:  un12  4106  unundi  4109  undif1  4415  dfif5  4481  tpcoma  4692  qdass  4695  qdassr  4696  tpidm12  4697  symdifv  5020  unidif0  5286  cnvimassrndm  6053  difxp2  6067  resasplit  6641  fresaun  6642  fresaunres2  6643  f1ofvswap  7172  df2o3  8294  sbthlem6  8855  fodomr  8895  domss2  8903  domunfican  9063  dftrpred4g  9480  kmlem11  9915  hashfun  14148  prmreclem2  16614  setscom  16877  gsummptfzsplitl  19530  uniioombllem3  24745  lhop  25176  ex-un  28782  ex-pw  28787  indifundif  30867  cycpmrn  31404  bnj1415  33012  subfacp1lem1  33135  sltlpss  34081  lineunray  34443  bj-2upln1upl  35208  poimirlem3  35774  poimirlem4  35775  poimirlem5  35776  poimirlem16  35787  poimirlem17  35788  poimirlem19  35790  poimirlem20  35791  poimirlem22  35793  metakunt24  40143  dfrcl2  41250  iunrelexp0  41278  trclfvdecomr  41304  corcltrcl  41315  cotrclrcl  41318  df3o2  41602  fourierdlem80  43696  caragenuncllem  44019  carageniuncllem1  44028  1fzopredsuc  44783  nnsum4primeseven  45219  nnsum4primesevenALTV  45220  lmod1  45800  iscnrm3rlem1  46201