Theorem uneq1i 4126

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

Syntax hints:   = wceq 1567   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918

This theorem is referenced by:  un12  4134  unundi  4137  undif1  4439  dfif5  4506  tpcoma  4718  qdass  4721  qdassr  4722  tpidm12  4723  symdifv  5053  unidif0OLD  5329  cnvimassrndm  6148  difxp2  6162  resasplit  6746  fresaun  6747  fresaunres2  6748  f1ofvswap  7302  df2o3  8457  sbthlem6  9076  fodomr  9112  domss2  9120  domunfican  9277  fodomfir  9283  kmlem11  10140  hashfun  14470  prmreclem2  16973  setscom  17236  gsummptfzsplitl  19999  uniioombllem3  25709  lhop  26140  ltslpss  28063  leslss  28064  addsasslem1  28158  mulsproplem5  28275  mulsproplem6  28276  mulsproplem7  28277  mulsproplem8  28278  ex-un  30712  ex-pw  30717  3unrab  32786  indifundif  32807  partfun2  32958  nn0split01  33099  cycpmrn  33400  evlextv  33873  esplyind  33906  esplyindfv  33907  vietalem  33910  bnj1415  35367  subfacp1lem1  35566  lineunray  36534  ttcun  36908  ttciun  36910  bj-2upln1upl  37544  poimirlem3  38157  poimirlem4  38158  poimirlem5  38159  poimirlem16  38170  poimirlem17  38171  poimirlem19  38173  poimirlem20  38174  poimirlem22  38176  dmxrnuncnvepres  38926  df3o2  43925  omcl3g  43946  dfrcl2  44285  iunrelexp0  44313  trclfvdecomr  44339  corcltrcl  44350  cotrclrcl  44353  fourierdlem80  46785  caragenuncllem  47111  carageniuncllem1  47120  1fzopredsuc  47944  nnsum4primeseven  48447  nnsum4primesevenALTV  48448  cycl3grtri  48594  usgrexmpl1edg  48671  usgrexmpl2edg  48676  gpgprismgr4cycllem7  48748  lmod1  49150  tposresg  49534  iscnrm3rlem1  49596