Theorem uneq1i 4117

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

Syntax hints:   = wceq 1540   ∪ cun 3903

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910

This theorem is referenced by:  un12  4126  unundi  4129  undif1  4429  dfif5  4495  tpcoma  4704  qdass  4707  qdassr  4708  tpidm12  4709  symdifv  5038  unidif0  5302  cnvimassrndm  6105  difxp2  6119  resasplit  6698  fresaun  6699  fresaunres2  6700  f1ofvswap  7247  df2o3  8403  sbthlem6  9016  fodomr  9052  domss2  9060  domunfican  9230  fodomfir  9237  kmlem11  10074  hashfun  14363  prmreclem2  16848  setscom  17110  gsummptfzsplitl  19831  dfcnfldOLD  21296  uniioombllem3  25503  lhop  25938  sltlpss  27841  slelss  27842  addsasslem1  27934  mulsproplem5  28047  mulsproplem6  28048  mulsproplem7  28049  mulsproplem8  28050  ex-un  30387  ex-pw  30392  3unrab  32466  indifundif  32487  nn0split01  32781  cycpmrn  33104  bnj1415  35024  subfacp1lem1  35171  lineunray  36140  bj-2upln1upl  37017  poimirlem3  37622  poimirlem4  37623  poimirlem5  37624  poimirlem16  37635  poimirlem17  37636  poimirlem19  37638  poimirlem20  37639  poimirlem22  37641  df3o2  43306  omcl3g  43327  dfrcl2  43667  iunrelexp0  43695  trclfvdecomr  43721  corcltrcl  43732  cotrclrcl  43735  fourierdlem80  46187  caragenuncllem  46513  carageniuncllem1  46522  1fzopredsuc  47328  nnsum4primeseven  47804  nnsum4primesevenALTV  47805  cycl3grtri  47951  usgrexmpl1edg  48028  usgrexmpl2edg  48033  gpgprismgr4cycllem7  48105  lmod1  48497  tposresg  48882  iscnrm3rlem1  48944