Theorem uneq12i 4166

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

Syntax hints:   = wceq 1540   ∪ cun 3949

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956

This theorem is referenced by:  indir  4286  difundir  4291  difindi  4292  dfsymdif3  4306  unrab  4315  rabun2  4324  elnelun  4393  dfif6  4528  dfif3  4540  dfif5  4542  symdif0  5085  symdifid  5087  unopab  5224  xpundi  5754  xpundir  5755  xpun  5759  dmun  5921  resundi  6011  resundir  6012  cnvun  6162  rnun  6165  imaundi  6169  imaundir  6170  dmtpop  6238  coundi  6267  coundir  6268  unidmrn  6299  dfdm2  6301  predun  6349  mptun  6714  partfun  6715  resasplit  6778  fresaun  6779  fresaunres2  6780  residpr  7163  fpr  7174  sbthlem5  9127  1sdomOLD  9285  djuassen  10219  fz0to3un2pr  13669  fz0to4untppr  13670  fz0to5un2tp  13671  fzo0to42pr  13792  hashgval  14372  hashinf  14374  relexpcnv  15074  bpoly3  16094  vdwlem6  17024  setsres  17215  lefld  18637  opsrtoslem1  22079  volun  25580  nosupcbv  27747  noinfcbv  27762  lrold  27935  addsval2  27996  addscut  28011  addsunif  28035  addsbday  28050  mulsval2  28137  muls01  28138  mulsproplem2  28143  mulsproplem3  28144  mulsproplem4  28145  mulscut  28158  mulsunif  28176  addsdilem1  28177  addsdilem2  28178  mulsasslem1  28189  mulsasslem2  28190  mulsunif2  28196  precsexlemcbv  28230  onaddscl  28286  onmulscl  28287  n0scut  28338  1p1e2s  28400  nohalf  28407  ex-dif  30442  ex-in  30444  ex-pw  30448  ex-xp  30455  ex-cnv  30456  ex-rn  30459  fzodif1  32794  indval2  32839  ordtprsuni  33918  sigaclfu2  34122  eulerpartgbij  34374  subfacp1lem1  35184  subfacp1lem5  35189  fmla1  35392  fixun  35910  refssfne  36359  onint1  36450  bj-pr1un  37004  bj-pr21val  37014  bj-pr2un  37018  bj-pr22val  37020  poimirlem16  37643  poimirlem19  37646  itg2addnclem2  37679  iblabsnclem  37690  redvmptabs  42390  df3o3  43327  rclexi  43628  rtrclex  43630  cnvrcl0  43638  dfrtrcl5  43642  dfrcl2  43687  dfrcl4  43689  iunrelexp0  43715  relexpiidm  43717  corclrcl  43720  relexp01min  43726  corcltrcl  43752  cotrclrcl  43755  frege131d  43777  rnfdmpr  47293  31prm  47584