Theorem uneq1i 4116

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

Syntax hints:   = wceq 1541   ∪ cun 3899

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906

This theorem is referenced by:  un12  4125  unundi  4128  undif1  4428  dfif5  4496  tpcoma  4707  qdass  4710  qdassr  4711  tpidm12  4712  symdifv  5041  unidif0  5305  cnvimassrndm  6110  difxp2  6124  resasplit  6704  fresaun  6705  fresaunres2  6706  f1ofvswap  7252  df2o3  8405  sbthlem6  9020  fodomr  9056  domss2  9064  domunfican  9222  fodomfir  9228  kmlem11  10071  hashfun  14360  prmreclem2  16845  setscom  17107  gsummptfzsplitl  19862  dfcnfldOLD  21325  uniioombllem3  25542  lhop  25977  ltslpss  27904  leslss  27905  addsasslem1  27999  mulsproplem5  28116  mulsproplem6  28117  mulsproplem7  28118  mulsproplem8  28119  ex-un  30499  ex-pw  30504  3unrab  32578  indifundif  32599  partfun2  32755  nn0split01  32898  cycpmrn  33225  evlextv  33707  esplyind  33731  esplyindfv  33732  vietalem  33735  bnj1415  35194  subfacp1lem1  35373  lineunray  36341  bj-2upln1upl  37225  poimirlem3  37824  poimirlem4  37825  poimirlem5  37826  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem22  37843  dmxrnuncnvepres  38577  df3o2  43555  omcl3g  43576  dfrcl2  43915  iunrelexp0  43943  trclfvdecomr  43969  corcltrcl  43980  cotrclrcl  43983  fourierdlem80  46430  caragenuncllem  46756  carageniuncllem1  46765  1fzopredsuc  47570  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  cycl3grtri  48193  usgrexmpl1edg  48270  usgrexmpl2edg  48275  gpgprismgr4cycllem7  48347  lmod1  48738  tposresg  49123  iscnrm3rlem1  49185