Theorem uneq12i 4120

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

Syntax hints:   = wceq 1542   ∪ cun 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908

This theorem is referenced by:  indir  4240  difundir  4245  difindi  4246  dfsymdif3  4260  unrab  4269  rabun2  4278  elnelun  4347  dfif6  4484  dfif3  4496  dfif5  4498  symdif0  5042  symdifid  5044  unopab  5180  xpundi  5701  xpundir  5702  xpun  5706  dmun  5867  resundi  5960  resundir  5961  cnvun  6108  rnun  6111  imaundi  6115  imaundir  6116  dmtpop  6184  coundi  6213  coundir  6214  unidmrn  6245  dfdm2  6247  predun  6294  mptun  6646  partfun  6647  resasplit  6712  fresaun  6713  fresaunres2  6714  residpr  7098  fpr  7109  sbthlem5  9031  djuassen  10101  fz0to3un2pr  13557  fz0to4untppr  13558  fz0to5un2tp  13559  fzo0to42pr  13681  hashgval  14268  hashinf  14270  relexpcnv  14970  bpoly3  15993  vdwlem6  16926  setsres  17117  lefld  18527  opsrtoslem1  22022  volun  25514  nosupcbv  27682  noinfcbv  27697  lrold  27905  addsval2  27971  addcuts  27986  addsunif  28010  addbday  28026  mulsval2  28119  muls01  28120  mulsproplem2  28125  mulsproplem3  28126  mulsproplem4  28127  mulcut  28140  mulsunif  28158  addsdilem1  28159  addsdilem2  28160  mulsasslem1  28171  mulsasslem2  28172  mulsunif2  28178  precsexlemcbv  28214  onaddscl  28285  onmulscl  28286  n0cut  28342  twocut  28431  bdaypw2n0bndlem  28471  0reno  28504  1reno  28505  ex-dif  30510  ex-in  30512  ex-pw  30516  ex-xp  30523  ex-cnv  30524  ex-rn  30527  fzodif1  32883  indval2  32944  indconst0  32950  ordtprsuni  34097  sigaclfu2  34299  eulerpartgbij  34550  subfacp1lem1  35395  subfacp1lem5  35400  fmla1  35603  fixun  36123  refssfne  36574  onint1  36665  bj-pr1un  37251  bj-pr21val  37261  bj-pr2un  37265  bj-pr22val  37267  poimirlem16  37887  poimirlem19  37890  itg2addnclem2  37923  iblabsnclem  37934  dfsucmap3  38714  redvmptabs  42730  df3o3  43671  rclexi  43971  rtrclex  43973  cnvrcl0  43981  dfrtrcl5  43985  dfrcl2  44030  dfrcl4  44032  iunrelexp0  44058  relexpiidm  44060  corclrcl  44063  relexp01min  44069  corcltrcl  44095  cotrclrcl  44098  frege131d  44120  rnfdmpr  47641  31prm  47957