Theorem uneq1i 4115

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

Syntax hints:   = wceq 1559   ∪ cun 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907

This theorem is referenced by:  un12  4123  unundi  4126  undif1  4427  dfif5  4494  tpcoma  4706  qdass  4709  qdassr  4710  tpidm12  4711  symdifv  5040  unidif0OLD  5314  cnvimassrndm  6133  difxp2  6147  resasplit  6729  fresaun  6730  fresaunres2  6731  f1ofvswap  7285  df2o3  8439  sbthlem6  9058  fodomr  9094  domss2  9102  domunfican  9260  fodomfir  9266  kmlem11  10111  hashfun  14444  prmreclem2  16944  setscom  17207  gsummptfzsplitl  19964  uniioombllem3  25635  lhop  26066  ltslpss  27989  leslss  27990  addsasslem1  28084  mulsproplem5  28201  mulsproplem6  28202  mulsproplem7  28203  mulsproplem8  28204  ex-un  30583  ex-pw  30588  3unrab  32662  indifundif  32683  partfun2  32839  nn0split01  32981  cycpmrn  33284  evlextv  33800  esplyind  33833  esplyindfv  33834  vietalem  33837  bnj1415  35294  subfacp1lem1  35490  lineunray  36458  ttcun  36833  ttciun  36835  bj-2upln1upl  37470  poimirlem3  38083  poimirlem4  38084  poimirlem5  38085  poimirlem16  38096  poimirlem17  38097  poimirlem19  38099  poimirlem20  38100  poimirlem22  38102  dmxrnuncnvepres  38852  df3o2  43851  omcl3g  43872  dfrcl2  44211  iunrelexp0  44239  trclfvdecomr  44265  corcltrcl  44276  cotrclrcl  44279  fourierdlem80  46721  caragenuncllem  47047  carageniuncllem1  47056  1fzopredsuc  47880  nnsum4primeseven  48383  nnsum4primesevenALTV  48384  cycl3grtri  48530  usgrexmpl1edg  48607  usgrexmpl2edg  48612  gpgprismgr4cycllem7  48684  lmod1  49075  tposresg  49460  iscnrm3rlem1  49522