Theorem uneq12i 4162

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

Syntax hints:   = wceq 1542   ∪ cun 3947

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 3954

This theorem is referenced by:  indir  4276  difundir  4281  difindi  4282  dfsymdif3  4297  unrab  4306  rabun2  4314  elnelun  4390  dfif6  4532  dfif3  4543  dfif5  4545  symdif0  5089  symdifid  5091  unopab  5231  xpundi  5745  xpundir  5746  xpun  5750  dmun  5911  resundi  5996  resundir  5997  cnvun  6143  rnun  6146  imaundi  6150  imaundir  6151  dmtpop  6218  coundi  6247  coundir  6248  unidmrn  6279  dfdm2  6281  predun  6330  mptun  6697  partfun  6698  resasplit  6762  fresaun  6763  fresaunres2  6764  residpr  7141  fpr  7152  sbthlem5  9087  1sdomOLD  9249  djuassen  10173  fz0to3un2pr  13603  fz0to4untppr  13604  fzo0to42pr  13719  hashgval  14293  hashinf  14295  relexpcnv  14982  bpoly3  16002  vdwlem6  16919  setsres  17111  lefld  18545  opsrtoslem1  21616  volun  25062  nosupcbv  27205  noinfcbv  27220  lrold  27391  addsval2  27447  addscut  27462  addsunif  27485  mulsval2  27567  muls01  27568  mulsproplem2  27573  mulsproplem3  27574  mulsproplem4  27575  mulscut  27588  mulsunif  27605  addsdilem1  27606  addsdilem2  27607  mulsasslem1  27618  mulsasslem2  27619  precsexlemcbv  27652  ex-dif  29676  ex-in  29678  ex-pw  29682  ex-xp  29689  ex-cnv  29690  ex-rn  29693  fzodif1  32004  ordtprsuni  32899  indval2  33012  sigaclfu2  33119  eulerpartgbij  33371  subfacp1lem1  34170  subfacp1lem5  34175  fmla1  34378  fixun  34881  refssfne  35243  onint1  35334  bj-pr1un  35884  bj-pr21val  35894  bj-pr2un  35898  bj-pr22val  35900  poimirlem16  36504  poimirlem19  36507  itg2addnclem2  36540  iblabsnclem  36551  df3o3  42064  rclexi  42366  rtrclex  42368  cnvrcl0  42376  dfrtrcl5  42380  dfrcl2  42425  dfrcl4  42427  iunrelexp0  42453  relexpiidm  42455  corclrcl  42458  relexp01min  42464  corcltrcl  42490  cotrclrcl  42493  frege131d  42515  rnfdmpr  45989  31prm  46265