Theorem uneq12i 4107

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

Syntax hints:   = wceq 1542   ∪ cun 3888

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 3432  df-un 3895

This theorem is referenced by:  indir  4227  difundir  4232  difindi  4233  dfsymdif3  4247  unrab  4256  rabun2  4265  elnelun  4334  dfif6  4470  dfif3  4482  dfif5  4484  symdif0  5028  symdifid  5030  unopab  5166  xpundi  5694  xpundir  5695  xpun  5699  dmun  5860  resundi  5953  resundir  5954  cnvun  6101  rnun  6104  imaundi  6108  imaundir  6109  dmtpop  6177  coundi  6206  coundir  6207  unidmrn  6238  dfdm2  6240  predun  6287  mptun  6639  partfun  6640  resasplit  6705  fresaun  6706  fresaunres2  6707  residpr  7091  fpr  7102  sbthlem5  9023  djuassen  10095  indval2  12158  indconst0  12165  fz0to3un2pr  13577  fz0to4untppr  13578  fz0to5un2tp  13579  fzo0to42pr  13702  hashgval  14289  hashinf  14291  relexpcnv  14991  bpoly3  16017  vdwlem6  16951  setsres  17142  lefld  18552  opsrtoslem1  22046  volun  25525  nosupcbv  27683  noinfcbv  27698  lrold  27906  addsval2  27972  addcuts  27987  addsunif  28011  addbday  28027  mulsval2  28120  muls01  28121  mulsproplem2  28126  mulsproplem3  28127  mulsproplem4  28128  mulcut  28141  mulsunif  28159  addsdilem1  28160  addsdilem2  28161  mulsasslem1  28172  mulsasslem2  28173  mulsunif2  28179  precsexlemcbv  28215  onaddscl  28286  onmulscl  28287  n0cut  28343  twocut  28432  bdaypw2n0bndlem  28472  0reno  28505  1reno  28506  ex-dif  30511  ex-in  30513  ex-pw  30517  ex-xp  30524  ex-cnv  30525  ex-rn  30528  fzodif1  32883  ordtprsuni  34082  sigaclfu2  34284  eulerpartgbij  34535  subfacp1lem1  35380  subfacp1lem5  35385  fmla1  35588  fixun  36108  refssfne  36559  onint1  36650  ttcun  36713  bj-pr1un  37329  bj-pr21val  37339  bj-pr2un  37343  bj-pr22val  37345  poimirlem16  37974  poimirlem19  37977  itg2addnclem2  38010  iblabsnclem  38021  dfsucmap3  38801  redvmptabs  42809  df3o3  43763  rclexi  44063  rtrclex  44065  cnvrcl0  44073  dfrtrcl5  44077  dfrcl2  44122  dfrcl4  44124  iunrelexp0  44150  relexpiidm  44152  corclrcl  44155  relexp01min  44161  corcltrcl  44187  cotrclrcl  44190  frege131d  44212  rnfdmpr  47744  31prm  48075