Theorem uneq12i 4161

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

Syntax hints:   = wceq 1542   ∪ cun 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3953

This theorem is referenced by:  indir  4275  difundir  4280  difindi  4281  dfsymdif3  4296  unrab  4305  rabun2  4313  elnelun  4389  dfif6  4531  dfif3  4542  dfif5  4544  symdif0  5088  symdifid  5090  unopab  5230  xpundi  5743  xpundir  5744  xpun  5748  dmun  5909  resundi  5994  resundir  5995  cnvun  6140  rnun  6143  imaundi  6147  imaundir  6148  dmtpop  6215  coundi  6244  coundir  6245  unidmrn  6276  dfdm2  6278  predun  6327  mptun  6694  partfun  6695  resasplit  6759  fresaun  6760  fresaunres2  6761  residpr  7138  fpr  7149  sbthlem5  9084  1sdomOLD  9246  djuassen  10170  fz0to3un2pr  13600  fz0to4untppr  13601  fzo0to42pr  13716  hashgval  14290  hashinf  14292  relexpcnv  14979  bpoly3  15999  vdwlem6  16916  setsres  17108  lefld  18542  opsrtoslem1  21608  volun  25054  nosupcbv  27195  noinfcbv  27210  lrold  27381  addsval2  27437  addscut  27452  addsunif  27475  mulsval2  27557  muls01  27558  mulsproplem2  27563  mulsproplem3  27564  mulsproplem4  27565  mulscut  27578  mulsunif  27595  addsdilem1  27596  addsdilem2  27597  mulsasslem1  27608  mulsasslem2  27609  precsexlemcbv  27642  ex-dif  29666  ex-in  29668  ex-pw  29672  ex-xp  29679  ex-cnv  29680  ex-rn  29683  fzodif1  31992  ordtprsuni  32888  indval2  33001  sigaclfu2  33108  eulerpartgbij  33360  subfacp1lem1  34159  subfacp1lem5  34164  fmla1  34367  fixun  34870  refssfne  35232  onint1  35323  bj-pr1un  35873  bj-pr21val  35883  bj-pr2un  35887  bj-pr22val  35889  poimirlem16  36493  poimirlem19  36496  itg2addnclem2  36529  iblabsnclem  36540  df3o3  42050  rclexi  42352  rtrclex  42354  cnvrcl0  42362  dfrtrcl5  42366  dfrcl2  42411  dfrcl4  42413  iunrelexp0  42439  relexpiidm  42441  corclrcl  42444  relexp01min  42450  corcltrcl  42476  cotrclrcl  42479  frege131d  42501  rnfdmpr  45976  31prm  46252