Theorem uneq1i 4113

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

Syntax hints:   = wceq 1541   ∪ cun 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903

This theorem is referenced by:  un12  4122  unundi  4125  undif1  4425  dfif5  4493  tpcoma  4704  qdass  4707  qdassr  4708  tpidm12  4709  symdifv  5038  unidif0  5302  cnvimassrndm  6107  difxp2  6121  resasplit  6701  fresaun  6702  fresaunres2  6703  f1ofvswap  7249  df2o3  8402  sbthlem6  9016  fodomr  9052  domss2  9060  domunfican  9217  fodomfir  9223  kmlem11  10063  hashfun  14351  prmreclem2  16836  setscom  17098  gsummptfzsplitl  19853  dfcnfldOLD  21316  uniioombllem3  25533  lhop  25968  sltlpss  27873  slelss  27874  addsasslem1  27966  mulsproplem5  28079  mulsproplem6  28080  mulsproplem7  28081  mulsproplem8  28082  ex-un  30425  ex-pw  30430  3unrab  32504  indifundif  32525  partfun2  32681  nn0split01  32826  cycpmrn  33153  evlextv  33635  esplyind  33659  esplyindfv  33660  vietalem  33663  bnj1415  35122  subfacp1lem1  35295  lineunray  36263  bj-2upln1upl  37141  poimirlem3  37736  poimirlem4  37737  poimirlem5  37738  poimirlem16  37749  poimirlem17  37750  poimirlem19  37752  poimirlem20  37753  poimirlem22  37755  dmxrnuncnvepres  38489  df3o2  43470  omcl3g  43491  dfrcl2  43831  iunrelexp0  43859  trclfvdecomr  43885  corcltrcl  43896  cotrclrcl  43899  fourierdlem80  46346  caragenuncllem  46672  carageniuncllem1  46681  1fzopredsuc  47486  nnsum4primeseven  47962  nnsum4primesevenALTV  47963  cycl3grtri  48109  usgrexmpl1edg  48186  usgrexmpl2edg  48191  gpgprismgr4cycllem7  48263  lmod1  48654  tposresg  49039  iscnrm3rlem1  49101