Theorem uneq1i 4094

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

Syntax hints:   = wceq 1547   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888

This theorem is referenced by:  un12  4102  unundi  4105  undif1  4404  dfif5  4471  tpcoma  4682  qdass  4685  qdassr  4686  tpidm12  4687  symdifv  5015  unidif0OLD  5289  cnvimassrndm  6103  difxp2  6117  resasplit  6697  fresaun  6698  fresaunres2  6699  f1ofvswap  7250  df2o3  8403  sbthlem6  9020  fodomr  9056  domss2  9064  domunfican  9222  fodomfir  9228  kmlem11  10074  hashfun  14390  prmreclem2  16879  setscom  17141  gsummptfzsplitl  19899  uniioombllem3  25570  lhop  26001  ltslpss  27918  leslss  27919  addsasslem1  28013  mulsproplem5  28130  mulsproplem6  28131  mulsproplem7  28132  mulsproplem8  28133  ex-un  30512  ex-pw  30517  3unrab  32591  indifundif  32612  partfun2  32768  nn0split01  32910  cycpmrn  33224  evlextv  33726  esplyind  33759  esplyindfv  33760  vietalem  33763  bnj1415  35220  subfacp1lem1  35407  lineunray  36375  ttcun  36740  ttciun  36742  bj-2upln1upl  37377  poimirlem3  37990  poimirlem4  37991  poimirlem5  37992  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem22  38009  dmxrnuncnvepres  38759  df3o2  43758  omcl3g  43779  dfrcl2  44118  iunrelexp0  44146  trclfvdecomr  44172  corcltrcl  44183  cotrclrcl  44186  fourierdlem80  46629  caragenuncllem  46955  carageniuncllem1  46964  1fzopredsuc  47788  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  cycl3grtri  48438  usgrexmpl1edg  48515  usgrexmpl2edg  48520  gpgprismgr4cycllem7  48592  lmod1  48983  tposresg  49368  iscnrm3rlem1  49430