Theorem uneq1i 4187

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

Syntax hints:   = wceq 1537   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981

This theorem is referenced by:  un12  4196  unundi  4199  undif1  4499  dfif5  4564  tpcoma  4775  qdass  4778  qdassr  4779  tpidm12  4780  symdifv  5109  unidif0  5378  cnvimassrndm  6183  difxp2  6197  resasplit  6791  fresaun  6792  fresaunres2  6793  f1ofvswap  7342  df2o3  8530  sbthlem6  9154  fodomr  9194  domss2  9202  domunfican  9389  fodomfir  9396  kmlem11  10230  hashfun  14486  prmreclem2  16964  setscom  17227  gsummptfzsplitl  19975  dfcnfldOLD  21403  uniioombllem3  25639  lhop  26075  sltlpss  27963  slelss  27964  addsasslem1  28054  mulsproplem5  28164  mulsproplem6  28165  mulsproplem7  28166  mulsproplem8  28167  ex-un  30456  ex-pw  30461  3unrab  32531  indifundif  32554  nn0split01  32821  cycpmrn  33136  bnj1415  35014  subfacp1lem1  35147  lineunray  36111  bj-2upln1upl  36990  poimirlem3  37583  poimirlem4  37584  poimirlem5  37585  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  metakunt24  42185  df3o2  43275  omcl3g  43296  dfrcl2  43636  iunrelexp0  43664  trclfvdecomr  43690  corcltrcl  43701  cotrclrcl  43704  fourierdlem80  46107  caragenuncllem  46433  carageniuncllem1  46442  1fzopredsuc  47239  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  usgrexmpl1edg  47839  usgrexmpl2edg  47844  lmod1  48221  iscnrm3rlem1  48620