Theorem uneq12i 4114

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

Syntax hints:   = wceq 1541   ∪ cun 3898

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 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-un 3905

This theorem is referenced by:  indir  4234  difundir  4239  difindi  4240  dfsymdif3  4254  unrab  4263  rabun2  4272  elnelun  4341  dfif6  4476  dfif3  4488  dfif5  4490  symdif0  5031  symdifid  5033  unopab  5169  xpundi  5683  xpundir  5684  xpun  5688  dmun  5848  resundi  5939  resundir  5940  cnvun  6086  rnun  6089  imaundi  6093  imaundir  6094  dmtpop  6162  coundi  6191  coundir  6192  unidmrn  6222  dfdm2  6224  predun  6271  mptun  6623  partfun  6624  resasplit  6689  fresaun  6690  fresaunres2  6691  residpr  7071  fpr  7082  sbthlem5  8999  djuassen  10062  fz0to3un2pr  13521  fz0to4untppr  13522  fz0to5un2tp  13523  fzo0to42pr  13645  hashgval  14232  hashinf  14234  relexpcnv  14934  bpoly3  15957  vdwlem6  16890  setsres  17081  lefld  18490  opsrtoslem1  21983  volun  25466  nosupcbv  27634  noinfcbv  27649  lrold  27835  addsval2  27899  addscut  27914  addsunif  27938  addsbday  27953  mulsval2  28043  muls01  28044  mulsproplem2  28049  mulsproplem3  28050  mulsproplem4  28051  mulscut  28064  mulsunif  28082  addsdilem1  28083  addsdilem2  28084  mulsasslem1  28095  mulsasslem2  28096  mulsunif2  28102  precsexlemcbv  28137  onaddscl  28203  onmulscl  28204  n0scut  28255  1p1e2s  28332  twocut  28339  ex-dif  30393  ex-in  30395  ex-pw  30399  ex-xp  30406  ex-cnv  30407  ex-rn  30410  fzodif1  32765  indval2  32825  ordtprsuni  33922  sigaclfu2  34124  eulerpartgbij  34375  subfacp1lem1  35191  subfacp1lem5  35196  fmla1  35399  fixun  35922  refssfne  36371  onint1  36462  bj-pr1un  37016  bj-pr21val  37026  bj-pr2un  37030  bj-pr22val  37032  poimirlem16  37655  poimirlem19  37658  itg2addnclem2  37691  iblabsnclem  37702  redvmptabs  42372  df3o3  43326  rclexi  43627  rtrclex  43629  cnvrcl0  43637  dfrtrcl5  43641  dfrcl2  43686  dfrcl4  43688  iunrelexp0  43714  relexpiidm  43716  corclrcl  43719  relexp01min  43725  corcltrcl  43751  cotrclrcl  43754  frege131d  43776  rnfdmpr  47291  31prm  47607