Theorem uneq12i 4175

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

Syntax hints:   = wceq 1536   ∪ cun 3960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967

This theorem is referenced by:  indir  4291  difundir  4296  difindi  4297  dfsymdif3  4311  unrab  4320  rabun2  4329  elnelun  4398  dfif6  4533  dfif3  4544  dfif5  4546  symdif0  5089  symdifid  5091  unopab  5229  xpundi  5756  xpundir  5757  xpun  5761  dmun  5923  resundi  6013  resundir  6014  cnvun  6164  rnun  6167  imaundi  6171  imaundir  6172  dmtpop  6239  coundi  6268  coundir  6269  unidmrn  6300  dfdm2  6302  predun  6350  mptun  6714  partfun  6715  resasplit  6778  fresaun  6779  fresaunres2  6780  residpr  7162  fpr  7173  sbthlem5  9125  1sdomOLD  9282  djuassen  10216  fz0to3un2pr  13665  fz0to4untppr  13666  fz0to5un2tp  13667  fzo0to42pr  13788  hashgval  14368  hashinf  14370  relexpcnv  15070  bpoly3  16090  vdwlem6  17019  setsres  17211  lefld  18649  opsrtoslem1  22096  volun  25593  nosupcbv  27761  noinfcbv  27776  lrold  27949  addsval2  28010  addscut  28025  addsunif  28049  addsbday  28064  mulsval2  28151  muls01  28152  mulsproplem2  28157  mulsproplem3  28158  mulsproplem4  28159  mulscut  28172  mulsunif  28190  addsdilem1  28191  addsdilem2  28192  mulsasslem1  28203  mulsasslem2  28204  mulsunif2  28210  precsexlemcbv  28244  onaddscl  28300  onmulscl  28301  n0scut  28352  1p1e2s  28414  nohalf  28421  ex-dif  30451  ex-in  30453  ex-pw  30457  ex-xp  30464  ex-cnv  30465  ex-rn  30468  fzodif1  32800  ordtprsuni  33879  indval2  33994  sigaclfu2  34101  eulerpartgbij  34353  subfacp1lem1  35163  subfacp1lem5  35168  fmla1  35371  fixun  35890  refssfne  36340  onint1  36431  bj-pr1un  36985  bj-pr21val  36995  bj-pr2un  36999  bj-pr22val  37001  poimirlem16  37622  poimirlem19  37625  itg2addnclem2  37658  iblabsnclem  37669  redvmptabs  42368  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  47230  31prm  47521