Theorem uneq12i 4117

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

Syntax hints:   = wceq 1540   ∪ cun 3901

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 3438  df-un 3908

This theorem is referenced by:  indir  4237  difundir  4242  difindi  4243  dfsymdif3  4257  unrab  4266  rabun2  4275  elnelun  4344  dfif6  4479  dfif3  4491  dfif5  4493  symdif0  5034  symdifid  5036  unopab  5172  xpundi  5688  xpundir  5689  xpun  5693  dmun  5853  resundi  5944  resundir  5945  cnvun  6091  rnun  6094  imaundi  6098  imaundir  6099  dmtpop  6167  coundi  6196  coundir  6197  unidmrn  6227  dfdm2  6229  predun  6276  mptun  6628  partfun  6629  resasplit  6694  fresaun  6695  fresaunres2  6696  residpr  7077  fpr  7088  sbthlem5  9008  djuassen  10073  fz0to3un2pr  13532  fz0to4untppr  13533  fz0to5un2tp  13534  fzo0to42pr  13656  hashgval  14240  hashinf  14242  relexpcnv  14942  bpoly3  15965  vdwlem6  16898  setsres  17089  lefld  18498  opsrtoslem1  21960  volun  25444  nosupcbv  27612  noinfcbv  27627  lrold  27811  addsval2  27875  addscut  27890  addsunif  27914  addsbday  27929  mulsval2  28019  muls01  28020  mulsproplem2  28025  mulsproplem3  28026  mulsproplem4  28027  mulscut  28040  mulsunif  28058  addsdilem1  28059  addsdilem2  28060  mulsasslem1  28071  mulsasslem2  28072  mulsunif2  28078  precsexlemcbv  28113  onaddscl  28179  onmulscl  28180  n0scut  28231  1p1e2s  28308  twocut  28315  ex-dif  30367  ex-in  30369  ex-pw  30373  ex-xp  30380  ex-cnv  30381  ex-rn  30384  fzodif1  32736  indval2  32798  ordtprsuni  33892  sigaclfu2  34094  eulerpartgbij  34346  subfacp1lem1  35162  subfacp1lem5  35167  fmla1  35370  fixun  35893  refssfne  36342  onint1  36433  bj-pr1un  36987  bj-pr21val  36997  bj-pr2un  37001  bj-pr22val  37003  poimirlem16  37626  poimirlem19  37629  itg2addnclem2  37662  iblabsnclem  37673  redvmptabs  42343  df3o3  43297  rclexi  43598  rtrclex  43600  cnvrcl0  43608  dfrtrcl5  43612  dfrcl2  43657  dfrcl4  43659  iunrelexp0  43685  relexpiidm  43687  corclrcl  43690  relexp01min  43696  corcltrcl  43722  cotrclrcl  43725  frege131d  43747  rnfdmpr  47275  31prm  47591