Theorem uneq1i 4109

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

Syntax hints:   = wceq 1541   ∪ cun 3895

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902

This theorem is referenced by:  un12  4118  unundi  4121  undif1  4421  dfif5  4487  tpcoma  4698  qdass  4701  qdassr  4702  tpidm12  4703  symdifv  5029  unidif0  5293  cnvimassrndm  6094  difxp2  6108  resasplit  6688  fresaun  6689  fresaunres2  6690  f1ofvswap  7235  df2o3  8388  sbthlem6  9000  fodomr  9036  domss2  9044  domunfican  9201  fodomfir  9207  kmlem11  10047  hashfun  14339  prmreclem2  16824  setscom  17086  gsummptfzsplitl  19840  dfcnfldOLD  21302  uniioombllem3  25508  lhop  25943  sltlpss  27848  slelss  27849  addsasslem1  27941  mulsproplem5  28054  mulsproplem6  28055  mulsproplem7  28056  mulsproplem8  28057  ex-un  30396  ex-pw  30401  3unrab  32475  indifundif  32496  nn0split01  32792  cycpmrn  33104  bnj1415  35042  subfacp1lem1  35215  lineunray  36181  bj-2upln1upl  37058  poimirlem3  37663  poimirlem4  37664  poimirlem5  37665  poimirlem16  37676  poimirlem17  37677  poimirlem19  37679  poimirlem20  37680  poimirlem22  37682  df3o2  43346  omcl3g  43367  dfrcl2  43707  iunrelexp0  43735  trclfvdecomr  43761  corcltrcl  43772  cotrclrcl  43775  fourierdlem80  46224  caragenuncllem  46550  carageniuncllem1  46559  1fzopredsuc  47355  nnsum4primeseven  47831  nnsum4primesevenALTV  47832  cycl3grtri  47978  usgrexmpl1edg  48055  usgrexmpl2edg  48060  gpgprismgr4cycllem7  48132  lmod1  48524  tposresg  48909  iscnrm3rlem1  48971