Theorem uneq1i 4163

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

This proof depends on syntax axioms:   = wceq 1569   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151

This theorem is used by:  un12  4171  unundi  4174  undif1  4429  dfif5  4498  tpcoma  4707  qdass  4710  qdassr  4711  tpidm12  4712  symdifv  5045  unidif0OLD  5321  difxp2  6156  cnvimassrndmOLD  6199  resasplit  6753  fresaun  6754  fresaunres2  6755  xpsntpg  7145  f1ofvswap  7315  df2o3  8488  sbthlem6  9115  fodomr  9151  domss2  9159  domunfican  9317  fodomfir  9323  kmlem11  10243  hashfun  14586  prmreclem2  17101  setscom  17364  gsummptfzsplitl  20153  uniioombllem3  25912  lhop  26342  ltslpss  28300  leslss  28301  addsasslem1  28395  mulsproplem5  28512  mulsproplem6  28513  mulsproplem7  28514  mulsproplem8  28515  ex-un  31031  ex-pw  31036  3unrab  33147  indifundif  33168  partfun2  33318  nn0split01  33456  cycpmrn  33751  evlextv  34221  esplyind  34254  esplyindfv  34255  vietalem  34258  bnj1415  35715  subfacp1lem1  36031  lineunray  37005  ttcun  37393  ttciun  37395  bj-2upln1upl  38030  poimirlem3  38635  poimirlem4  38636  poimirlem5  38637  poimirlem16  38648  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  poimirlem22  38654  dmxrnuncnvepres  39418  df3o2  44409  omcl3g  44430  dfrcl2  44768  iunrelexp0  44796  trclfvdecomr  44822  corcltrcl  44833  cotrclrcl  44836  fourierdlem80  47290  caragenuncllem  47616  carageniuncllem1  47625  1fzopredsuc  48489  nnsum4primeseven  48992  nnsum4primesevenALTV  48993  cycl3grtri  49139  usgrexmpl1edg  49216  usgrexmpl2edg  49221  gpgprismgr4cycllem7  49293  lmod1  49698  tposresg  50085  iscnrm3rlem1  50148