Theorem uneq12i 4129

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 4126	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
4	1, 2, 3	mp2an 692	1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷)

Syntax hints:   = wceq 1540   ∪ cun 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919

This theorem is referenced by:  indir  4249  difundir  4254  difindi  4255  dfsymdif3  4269  unrab  4278  rabun2  4287  elnelun  4356  dfif6  4491  dfif3  4503  dfif5  4505  symdif0  5049  symdifid  5051  unopab  5187  xpundi  5707  xpundir  5708  xpun  5712  dmun  5874  resundi  5964  resundir  5965  cnvun  6115  rnun  6118  imaundi  6122  imaundir  6123  dmtpop  6191  coundi  6220  coundir  6221  unidmrn  6252  dfdm2  6254  predun  6301  mptun  6664  partfun  6665  resasplit  6730  fresaun  6731  fresaunres2  6732  residpr  7115  fpr  7126  sbthlem5  9055  1sdomOLD  9196  djuassen  10132  fz0to3un2pr  13590  fz0to4untppr  13591  fz0to5un2tp  13592  fzo0to42pr  13714  hashgval  14298  hashinf  14300  relexpcnv  15001  bpoly3  16024  vdwlem6  16957  setsres  17148  lefld  18551  opsrtoslem1  21962  volun  25446  nosupcbv  27614  noinfcbv  27629  lrold  27808  addsval2  27870  addscut  27885  addsunif  27909  addsbday  27924  mulsval2  28014  muls01  28015  mulsproplem2  28020  mulsproplem3  28021  mulsproplem4  28022  mulscut  28035  mulsunif  28053  addsdilem1  28054  addsdilem2  28055  mulsasslem1  28066  mulsasslem2  28067  mulsunif2  28073  precsexlemcbv  28108  onaddscl  28174  onmulscl  28175  n0scut  28226  1p1e2s  28302  twocut  28309  ex-dif  30352  ex-in  30354  ex-pw  30358  ex-xp  30365  ex-cnv  30366  ex-rn  30369  fzodif1  32715  indval2  32777  ordtprsuni  33909  sigaclfu2  34111  eulerpartgbij  34363  subfacp1lem1  35166  subfacp1lem5  35171  fmla1  35374  fixun  35897  refssfne  36346  onint1  36437  bj-pr1un  36991  bj-pr21val  37001  bj-pr2un  37005  bj-pr22val  37007  poimirlem16  37630  poimirlem19  37633  itg2addnclem2  37666  iblabsnclem  37677  redvmptabs  42348  df3o3  43303  rclexi  43604  rtrclex  43606  cnvrcl0  43614  dfrtrcl5  43618  dfrcl2  43663  dfrcl4  43665  iunrelexp0  43691  relexpiidm  43693  corclrcl  43696  relexp01min  43702  corcltrcl  43728  cotrclrcl  43731  frege131d  43753  rnfdmpr  47282  31prm  47598