Theorem uneq1i 4144

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

Syntax hints:   = wceq 1540   ∪ cun 3929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936

This theorem is referenced by:  un12  4153  unundi  4156  undif1  4456  dfif5  4522  tpcoma  4731  qdass  4734  qdassr  4735  tpidm12  4736  symdifv  5067  unidif0  5335  cnvimassrndm  6146  difxp2  6160  resasplit  6753  fresaun  6754  fresaunres2  6755  f1ofvswap  7304  df2o3  8493  sbthlem6  9107  fodomr  9147  domss2  9155  domunfican  9338  fodomfir  9345  kmlem11  10180  hashfun  14460  prmreclem2  16942  setscom  17204  gsummptfzsplitl  19919  dfcnfldOLD  21336  uniioombllem3  25543  lhop  25978  sltlpss  27876  slelss  27877  addsasslem1  27967  mulsproplem5  28080  mulsproplem6  28081  mulsproplem7  28082  mulsproplem8  28083  ex-un  30410  ex-pw  30415  3unrab  32489  indifundif  32510  nn0split01  32801  cycpmrn  33159  bnj1415  35074  subfacp1lem1  35206  lineunray  36170  bj-2upln1upl  37047  poimirlem3  37652  poimirlem4  37653  poimirlem5  37654  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem20  37669  poimirlem22  37671  df3o2  43304  omcl3g  43325  dfrcl2  43665  iunrelexp0  43693  trclfvdecomr  43719  corcltrcl  43730  cotrclrcl  43733  fourierdlem80  46182  caragenuncllem  46508  carageniuncllem1  46517  1fzopredsuc  47320  nnsum4primeseven  47781  nnsum4primesevenALTV  47782  cycl3grtri  47926  usgrexmpl1edg  47995  usgrexmpl2edg  48000  gpgprismgr4cycllem7  48067  lmod1  48435  tposresg  48820  iscnrm3rlem1  48881