Theorem uneq12i 4113

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

Syntax hints:   = wceq 1541   ∪ cun 3895

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902

This theorem is referenced by:  indir  4233  difundir  4238  difindi  4239  dfsymdif3  4253  unrab  4262  rabun2  4271  elnelun  4340  dfif6  4475  dfif3  4487  dfif5  4489  symdif0  5031  symdifid  5033  unopab  5169  xpundi  5683  xpundir  5684  xpun  5688  dmun  5849  resundi  5941  resundir  5942  cnvun  6089  rnun  6092  imaundi  6096  imaundir  6097  dmtpop  6165  coundi  6194  coundir  6195  unidmrn  6226  dfdm2  6228  predun  6275  mptun  6627  partfun  6628  resasplit  6693  fresaun  6694  fresaunres2  6695  residpr  7076  fpr  7087  sbthlem5  9004  djuassen  10070  fz0to3un2pr  13529  fz0to4untppr  13530  fz0to5un2tp  13531  fzo0to42pr  13653  hashgval  14240  hashinf  14242  relexpcnv  14942  bpoly3  15965  vdwlem6  16898  setsres  17089  lefld  18498  opsrtoslem1  21990  volun  25473  nosupcbv  27641  noinfcbv  27656  lrold  27842  addsval2  27906  addscut  27921  addsunif  27945  addsbday  27960  mulsval2  28050  muls01  28051  mulsproplem2  28056  mulsproplem3  28057  mulsproplem4  28058  mulscut  28071  mulsunif  28089  addsdilem1  28090  addsdilem2  28091  mulsasslem1  28102  mulsasslem2  28103  mulsunif2  28109  precsexlemcbv  28144  onaddscl  28210  onmulscl  28211  n0scut  28262  1p1e2s  28339  twocut  28346  ex-dif  30403  ex-in  30405  ex-pw  30409  ex-xp  30416  ex-cnv  30417  ex-rn  30420  fzodif1  32775  indval2  32835  ordtprsuni  33932  sigaclfu2  34134  eulerpartgbij  34385  subfacp1lem1  35223  subfacp1lem5  35228  fmla1  35431  fixun  35951  refssfne  36402  onint1  36493  bj-pr1un  37047  bj-pr21val  37057  bj-pr2un  37061  bj-pr22val  37063  poimirlem16  37686  poimirlem19  37689  itg2addnclem2  37722  iblabsnclem  37733  dfsucmap3  38486  redvmptabs  42463  df3o3  43417  rclexi  43718  rtrclex  43720  cnvrcl0  43728  dfrtrcl5  43732  dfrcl2  43777  dfrcl4  43779  iunrelexp0  43805  relexpiidm  43807  corclrcl  43810  relexp01min  43816  corcltrcl  43842  cotrclrcl  43845  frege131d  43867  rnfdmpr  47391  31prm  47707