Theorem uneq12i 4106

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

Syntax hints:   = wceq 1542   ∪ cun 3887

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894

This theorem is referenced by:  indir  4226  difundir  4231  difindi  4232  dfsymdif3  4246  unrab  4255  rabun2  4264  elnelun  4333  dfif6  4469  dfif3  4481  dfif5  4483  symdif0  5027  symdifid  5029  unopab  5165  xpundi  5700  xpundir  5701  xpun  5705  dmun  5865  resundi  5958  resundir  5959  cnvun  6106  rnun  6109  imaundi  6113  imaundir  6114  dmtpop  6182  coundi  6211  coundir  6212  unidmrn  6243  dfdm2  6245  predun  6292  mptun  6644  partfun  6645  resasplit  6710  fresaun  6711  fresaunres2  6712  residpr  7096  fpr  7108  sbthlem5  9029  djuassen  10101  indval2  12164  indconst0  12171  fz0to3un2pr  13583  fz0to4untppr  13584  fz0to5un2tp  13585  fzo0to42pr  13708  hashgval  14295  hashinf  14297  relexpcnv  14997  bpoly3  16023  vdwlem6  16957  setsres  17148  lefld  18558  opsrtoslem1  22033  volun  25512  nosupcbv  27666  noinfcbv  27681  lrold  27889  addsval2  27955  addcuts  27970  addsunif  27994  addbday  28010  mulsval2  28103  muls01  28104  mulsproplem2  28109  mulsproplem3  28110  mulsproplem4  28111  mulcut  28124  mulsunif  28142  addsdilem1  28143  addsdilem2  28144  mulsasslem1  28155  mulsasslem2  28156  mulsunif2  28162  precsexlemcbv  28198  onaddscl  28269  onmulscl  28270  n0cut  28326  twocut  28415  bdaypw2n0bndlem  28455  0reno  28488  1reno  28489  ex-dif  30493  ex-in  30495  ex-pw  30499  ex-xp  30506  ex-cnv  30507  ex-rn  30510  fzodif1  32865  ordtprsuni  34063  sigaclfu2  34265  eulerpartgbij  34516  subfacp1lem1  35361  subfacp1lem5  35366  fmla1  35569  fixun  36089  refssfne  36540  onint1  36631  ttcun  36694  bj-pr1un  37310  bj-pr21val  37320  bj-pr2un  37324  bj-pr22val  37326  poimirlem16  37957  poimirlem19  37960  itg2addnclem2  37993  iblabsnclem  38004  dfsucmap3  38784  redvmptabs  42792  df3o3  43742  rclexi  44042  rtrclex  44044  cnvrcl0  44052  dfrtrcl5  44056  dfrcl2  44101  dfrcl4  44103  iunrelexp0  44129  relexpiidm  44131  corclrcl  44134  relexp01min  44140  corcltrcl  44166  cotrclrcl  44169  frege131d  44191  rnfdmpr  47729  31prm  48060