Theorem uneq1i 4158

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

Syntax hints:   = wceq 1539   ∪ cun 3945

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3952

This theorem is referenced by:  un12  4166  unundi  4169  undif1  4474  dfif5  4543  tpcoma  4753  qdass  4756  qdassr  4757  tpidm12  4758  symdifv  5088  unidif0  5357  cnvimassrndm  6150  difxp2  6164  resasplit  6760  fresaun  6761  fresaunres2  6762  f1ofvswap  7306  df2o3  8476  sbthlem6  9090  fodomr  9130  domss2  9138  domunfican  9322  kmlem11  10157  hashfun  14401  prmreclem2  16854  setscom  17117  gsummptfzsplitl  19842  uniioombllem3  25334  lhop  25768  sltlpss  27638  slelss  27639  addsasslem1  27725  mulsproplem5  27815  mulsproplem6  27816  mulsproplem7  27817  mulsproplem8  27818  ex-un  29944  ex-pw  29949  indifundif  32029  cycpmrn  32572  bnj1415  34347  subfacp1lem1  34468  lineunray  35423  gg-dfcnfld  35473  bj-2upln1upl  36208  poimirlem3  36794  poimirlem4  36795  poimirlem5  36796  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  poimirlem22  36813  metakunt24  41314  df3o2  42365  omcl3g  42386  dfrcl2  42727  iunrelexp0  42755  trclfvdecomr  42781  corcltrcl  42792  cotrclrcl  42795  fourierdlem80  45200  caragenuncllem  45526  carageniuncllem1  45535  1fzopredsuc  46330  nnsum4primeseven  46766  nnsum4primesevenALTV  46767  lmod1  47260  iscnrm3rlem1  47660