Theorem uneq1i 4133

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

Syntax hints:   = wceq 1531   ∪ cun 3932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-un 3939

This theorem is referenced by:  un12  4141  unundi  4144  undif1  4422  dfif5  4481  tpcoma  4678  qdass  4681  qdassr  4682  tpidm12  4683  symdifv  4999  unidif0  5251  difxp2  6016  resasplit  6541  fresaun  6542  fresaunres2  6543  df2o3  8109  sbthlem6  8624  fodomr  8660  domss2  8668  domunfican  8783  kmlem11  9578  hashfun  13790  prmreclem2  16245  setscom  16519  gsummptfzsplitl  19045  uniioombllem3  24178  lhop  24605  ex-un  28195  ex-pw  28200  indifundif  30277  cycpmrn  30778  bnj1415  32303  subfacp1lem1  32419  dftrpred4g  33066  lineunray  33601  bj-2upln1upl  34329  poimirlem3  34887  poimirlem4  34888  poimirlem5  34889  poimirlem16  34900  poimirlem17  34901  poimirlem19  34903  poimirlem20  34904  poimirlem22  34906  dfrcl2  40009  iunrelexp0  40037  trclfvdecomr  40063  corcltrcl  40074  cotrclrcl  40077  df3o2  40364  fourierdlem80  42461  caragenuncllem  42784  carageniuncllem1  42793  1fzopredsuc  43514  nnsum4primeseven  43955  nnsum4primesevenALTV  43956  lmod1  44537