Theorem uneq1i 4123

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

Syntax hints:   = wceq 1540   ∪ cun 3909

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 3446  df-un 3916

This theorem is referenced by:  un12  4132  unundi  4135  undif1  4435  dfif5  4501  tpcoma  4710  qdass  4713  qdassr  4714  tpidm12  4715  symdifv  5045  unidif0  5310  cnvimassrndm  6113  difxp2  6127  resasplit  6712  fresaun  6713  fresaunres2  6714  f1ofvswap  7263  df2o3  8419  sbthlem6  9033  fodomr  9069  domss2  9077  domunfican  9248  fodomfir  9255  kmlem11  10090  hashfun  14378  prmreclem2  16864  setscom  17126  gsummptfzsplitl  19839  dfcnfldOLD  21256  uniioombllem3  25462  lhop  25897  sltlpss  27795  slelss  27796  addsasslem1  27886  mulsproplem5  27999  mulsproplem6  28000  mulsproplem7  28001  mulsproplem8  28002  ex-un  30326  ex-pw  30331  3unrab  32405  indifundif  32426  nn0split01  32715  cycpmrn  33073  bnj1415  35001  subfacp1lem1  35139  lineunray  36108  bj-2upln1upl  36985  poimirlem3  37590  poimirlem4  37591  poimirlem5  37592  poimirlem16  37603  poimirlem17  37604  poimirlem19  37606  poimirlem20  37607  poimirlem22  37609  df3o2  43275  omcl3g  43296  dfrcl2  43636  iunrelexp0  43664  trclfvdecomr  43690  corcltrcl  43701  cotrclrcl  43704  fourierdlem80  46157  caragenuncllem  46483  carageniuncllem1  46492  1fzopredsuc  47298  nnsum4primeseven  47774  nnsum4primesevenALTV  47775  cycl3grtri  47919  usgrexmpl1edg  47988  usgrexmpl2edg  47993  gpgprismgr4cycllem7  48064  lmod1  48454  tposresg  48839  iscnrm3rlem1  48901