Theorem uneq12i 4128

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 4125	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
4	1, 2, 3	mp2an 704	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:  indir  4247  difundir  4252  difindi  4253  dfsymdif3  4267  unrab  4276  rabun2  4285  elnelun  4357  dfif6  4495  dfif3  4507  dfif5  4509  symdif0  5055  symdifid  5057  unopab  5195  xpundi  5731  xpundir  5732  xpun  5736  dmun  5901  resundi  5993  resundir  5994  cnvun  6140  rnun  6143  imaundi  6148  imaundir  6149  dmtpop  6220  coundi  6249  coundir  6250  unidmrn  6281  dfdm2  6283  predun  6330  mptun  6682  partfun  6683  resasplit  6749  fresaun  6750  fresaunres2  6751  residpr  7140  fpr  7152  sbthlem5  9079  djuassen  10162  indval2  12223  indconst0  12230  fz0to3un2pr  13657  fz0to4untppr  13658  fz0to5un2tp  13659  fzo0to42pr  13782  hashgval  14369  hashinf  14371  relexpcnv  15072  bpoly3  16112  vdwlem6  17046  setsres  17238  lefld  18648  opsrtoslem1  22175  volun  25673  nosupcbv  27832  noinfcbv  27847  lrold  28056  addsval2  28122  addcuts  28137  addsunif  28161  addbday  28177  mulsval2  28270  muls01  28271  mulsproplem2  28276  mulsproplem3  28277  mulsproplem4  28278  mulcut  28291  mulsunif  28309  addsdilem1  28310  addsdilem2  28311  mulsasslem1  28322  mulsasslem2  28323  mulsunif2  28329  precsexlemcbv  28365  onaddscl  28436  onmulscl  28437  n0cut  28493  twocut  28582  bdaypw2n0bndlem  28622  0reno  28655  1reno  28656  ex-dif  30715  ex-in  30717  ex-pw  30721  ex-xp  30728  ex-cnv  30729  ex-rn  30732  fzodif1  33078  ordtprsuni  34254  sigaclfu2  34456  eulerpartgbij  34707  subfacp1lem1  35570  subfacp1lem5  35575  fmla1  35778  fixun  36298  refssfne  36758  onint1  36849  ttcun  36912  bj-pr1un  37527  bj-pr21val  37537  bj-pr2un  37541  bj-pr22val  37543  poimirlem16  38175  poimirlem19  38178  itg2addnclem2  38211  iblabsnclem  38222  dfsucmap3  39002  redvmptabs  43011  df3o3  43933  rclexi  44233  rtrclex  44235  cnvrcl0  44243  dfrtrcl5  44247  dfrcl2  44292  dfrcl4  44294  iunrelexp0  44320  relexpiidm  44322  corclrcl  44325  relexp01min  44331  corcltrcl  44357  cotrclrcl  44360  frege131d  44382  rnfdmpr  47907  31prm  48238