Theorem uneq12i 4120

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

Syntax hints:   = wceq 1570   ∪ cun 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910

This theorem is referenced by:  indir  4239  difundir  4244  difindi  4245  dfsymdif3  4259  unrab  4268  rabun2  4277  elnelun  4350  dfif6  4490  dfif3  4502  dfif5  4504  symdif0  5051  symdifid  5053  unopab  5191  xpundi  5730  xpundir  5731  xpun  5735  dmun  5900  resundi  5992  resundir  5993  cnvun  6139  rnun  6142  imaundi  6147  imaundir  6148  dmtpop  6219  coundi  6248  coundir  6249  unidmrn  6280  dfdm2  6282  predun  6329  mptun  6681  partfun  6682  resasplit  6748  fresaun  6749  fresaunres2  6750  residpr  7139  fpr  7151  sbthlem5  9075  djuassen  10158  indval2  12218  indconst0  12225  fz0to3un2pr  13653  fz0to4untppr  13654  fz0to5un2tp  13655  fzo0to42pr  13778  hashgval  14365  hashinf  14367  relexpcnv  15068  bpoly3  16107  vdwlem6  17041  setsres  17233  lefld  18643  opsrtoslem1  22206  volun  25704  nosupcbv  27866  noinfcbv  27881  lrold  28090  addsval2  28156  addcuts  28171  addsunif  28195  addbday  28211  mulsval2  28304  muls01  28305  mulsproplem2  28310  mulsproplem3  28311  mulsproplem4  28312  mulcut  28325  mulsunif  28343  addsdilem1  28344  addsdilem2  28345  mulsasslem1  28356  mulsasslem2  28357  mulsunif2  28363  precsexlemcbv  28399  onaddscl  28470  onmulscl  28471  n0cut  28527  twocut  28616  bdaypw2n0bndlem  28656  0reno  28689  1reno  28690  ex-dif  30774  ex-in  30776  ex-pw  30780  ex-xp  30787  ex-cnv  30788  ex-rn  30791  fzodif1  33137  ordtprsuni  34309  sigaclfu2  34511  eulerpartgbij  34762  subfacp1lem1  35671  subfacp1lem5  35676  fmla1  35879  fixun  36399  refssfne  36889  onint1  36980  ttcun  37043  bj-pr1un  37659  bj-pr21val  37669  bj-pr2un  37673  bj-pr22val  37675  poimirlem16  38307  poimirlem19  38310  itg2addnclem2  38343  iblabsnclem  38354  dfsucmap3  39132  redvmptabs  43141  df3o3  44061  rclexi  44361  rtrclex  44363  cnvrcl0  44371  dfrtrcl5  44375  dfrcl2  44420  dfrcl4  44422  iunrelexp0  44448  relexpiidm  44450  corclrcl  44453  relexp01min  44459  corcltrcl  44485  cotrclrcl  44488  frege131d  44510  rnfdmpr  48038  31prm  48369