Theorem uneq12i 4125

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

Syntax hints:   = wceq 1540   ∪ cun 3909

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916

This theorem is referenced by:  indir  4245  difundir  4250  difindi  4251  dfsymdif3  4265  unrab  4274  rabun2  4283  elnelun  4352  dfif6  4487  dfif3  4499  dfif5  4501  symdif0  5044  symdifid  5046  unopab  5182  xpundi  5700  xpundir  5701  xpun  5705  dmun  5864  resundi  5953  resundir  5954  cnvun  6103  rnun  6106  imaundi  6110  imaundir  6111  dmtpop  6179  coundi  6208  coundir  6209  unidmrn  6240  dfdm2  6242  predun  6289  mptun  6646  partfun  6647  resasplit  6712  fresaun  6713  fresaunres2  6714  residpr  7097  fpr  7108  sbthlem5  9032  1sdomOLD  9172  djuassen  10108  fz0to3un2pr  13566  fz0to4untppr  13567  fz0to5un2tp  13568  fzo0to42pr  13690  hashgval  14274  hashinf  14276  relexpcnv  14977  bpoly3  16000  vdwlem6  16933  setsres  17124  lefld  18533  opsrtoslem1  21995  volun  25479  nosupcbv  27647  noinfcbv  27662  lrold  27846  addsval2  27910  addscut  27925  addsunif  27949  addsbday  27964  mulsval2  28054  muls01  28055  mulsproplem2  28060  mulsproplem3  28061  mulsproplem4  28062  mulscut  28075  mulsunif  28093  addsdilem1  28094  addsdilem2  28095  mulsasslem1  28106  mulsasslem2  28107  mulsunif2  28113  precsexlemcbv  28148  onaddscl  28214  onmulscl  28215  n0scut  28266  1p1e2s  28343  twocut  28350  ex-dif  30402  ex-in  30404  ex-pw  30408  ex-xp  30415  ex-cnv  30416  ex-rn  30419  fzodif1  32765  indval2  32827  ordtprsuni  33902  sigaclfu2  34104  eulerpartgbij  34356  subfacp1lem1  35159  subfacp1lem5  35164  fmla1  35367  fixun  35890  refssfne  36339  onint1  36430  bj-pr1un  36984  bj-pr21val  36994  bj-pr2un  36998  bj-pr22val  37000  poimirlem16  37623  poimirlem19  37626  itg2addnclem2  37659  iblabsnclem  37670  redvmptabs  42341  df3o3  43296  rclexi  43597  rtrclex  43599  cnvrcl0  43607  dfrtrcl5  43611  dfrcl2  43656  dfrcl4  43658  iunrelexp0  43684  relexpiidm  43686  corclrcl  43689  relexp01min  43695  corcltrcl  43721  cotrclrcl  43724  frege131d  43746  rnfdmpr  47275  31prm  47591