Theorem uneq12i 4116

Description: Equality inference for the union of two classes. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
uneq1i.1	⊢ 𝐴 = 𝐵
uneq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
uneq12i	⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)

Proof of Theorem uneq12i

Step	Hyp	Ref	Expression
1		uneq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		uneq12i.2	. 2 ⊢ 𝐶 = 𝐷
3		uneq12 4113	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
4	1, 2, 3	mp2an 692	1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)

Syntax hints:   = wceq 1541   ∪ cun 3897

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 2706

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 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904

This theorem is referenced by:  indir  4236  difundir  4241  difindi  4242  dfsymdif3  4256  unrab  4265  rabun2  4274  elnelun  4343  dfif6  4480  dfif3  4492  dfif5  4494  symdif0  5038  symdifid  5040  unopab  5176  xpundi  5691  xpundir  5692  xpun  5696  dmun  5857  resundi  5950  resundir  5951  cnvun  6098  rnun  6101  imaundi  6105  imaundir  6106  dmtpop  6174  coundi  6203  coundir  6204  unidmrn  6235  dfdm2  6237  predun  6284  mptun  6636  partfun  6637  resasplit  6702  fresaun  6703  fresaunres2  6704  residpr  7086  fpr  7097  sbthlem5  9017  djuassen  10087  fz0to3un2pr  13543  fz0to4untppr  13544  fz0to5un2tp  13545  fzo0to42pr  13667  hashgval  14254  hashinf  14256  relexpcnv  14956  bpoly3  15979  vdwlem6  16912  setsres  17103  lefld  18513  opsrtoslem1  22008  volun  25500  nosupcbv  27668  noinfcbv  27683  lrold  27869  addsval2  27933  addscut  27948  addsunif  27972  addsbday  27987  mulsval2  28080  muls01  28081  mulsproplem2  28086  mulsproplem3  28087  mulsproplem4  28088  mulscut  28101  mulsunif  28119  addsdilem1  28120  addsdilem2  28121  mulsasslem1  28132  mulsasslem2  28133  mulsunif2  28139  precsexlemcbv  28174  onaddscl  28241  onmulscl  28242  n0scut  28294  1p1e2s  28374  twocut  28381  bdaypw2n0s  28420  0reno  28441  1reno  28442  ex-dif  30447  ex-in  30449  ex-pw  30453  ex-xp  30460  ex-cnv  30461  ex-rn  30464  fzodif1  32821  indval2  32882  indconst0  32888  ordtprsuni  34025  sigaclfu2  34227  eulerpartgbij  34478  subfacp1lem1  35322  subfacp1lem5  35327  fmla1  35530  fixun  36050  refssfne  36501  onint1  36592  bj-pr1un  37147  bj-pr21val  37157  bj-pr2un  37161  bj-pr22val  37163  poimirlem16  37776  poimirlem19  37779  itg2addnclem2  37812  iblabsnclem  37823  dfsucmap3  38576  redvmptabs  42557  df3o3  43498  rclexi  43798  rtrclex  43800  cnvrcl0  43808  dfrtrcl5  43812  dfrcl2  43857  dfrcl4  43859  iunrelexp0  43885  relexpiidm  43887  corclrcl  43890  relexp01min  43896  corcltrcl  43922  cotrclrcl  43925  frege131d  43947  rnfdmpr  47469  31prm  47785