Theorem uneq12i 4160

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

Syntax hints:   = wceq 1539   ∪ cun 3945

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3952

This theorem is referenced by:  indir  4274  difundir  4279  difindi  4280  dfsymdif3  4295  unrab  4304  rabun2  4312  elnelun  4388  dfif6  4530  dfif3  4541  dfif5  4543  symdif0  5087  symdifid  5089  unopab  5229  xpundi  5743  xpundir  5744  xpun  5748  dmun  5909  resundi  5994  resundir  5995  cnvun  6141  rnun  6144  imaundi  6148  imaundir  6149  dmtpop  6216  coundi  6245  coundir  6246  unidmrn  6277  dfdm2  6279  predun  6328  mptun  6695  partfun  6696  resasplit  6760  fresaun  6761  fresaunres2  6762  residpr  7142  fpr  7153  sbthlem5  9089  1sdomOLD  9251  djuassen  10175  fz0to3un2pr  13607  fz0to4untppr  13608  fzo0to42pr  13723  hashgval  14297  hashinf  14299  relexpcnv  14986  bpoly3  16006  vdwlem6  16923  setsres  17115  lefld  18549  opsrtoslem1  21835  volun  25294  nosupcbv  27441  noinfcbv  27456  lrold  27628  addsval2  27685  addscut  27700  addsunif  27724  mulsval2  27806  muls01  27807  mulsproplem2  27812  mulsproplem3  27813  mulsproplem4  27814  mulscut  27827  mulsunif  27844  addsdilem1  27845  addsdilem2  27846  mulsasslem1  27857  mulsasslem2  27858  precsexlemcbv  27891  n0scut  27943  ex-dif  29943  ex-in  29945  ex-pw  29949  ex-xp  29956  ex-cnv  29957  ex-rn  29960  fzodif1  32271  ordtprsuni  33197  indval2  33310  sigaclfu2  33417  eulerpartgbij  33669  subfacp1lem1  34468  subfacp1lem5  34473  fmla1  34676  fixun  35185  refssfne  35546  onint1  35637  bj-pr1un  36187  bj-pr21val  36197  bj-pr2un  36201  bj-pr22val  36203  poimirlem16  36807  poimirlem19  36810  itg2addnclem2  36843  iblabsnclem  36854  df3o3  42366  rclexi  42668  rtrclex  42670  cnvrcl0  42678  dfrtrcl5  42682  dfrcl2  42727  dfrcl4  42729  iunrelexp0  42755  relexpiidm  42757  corclrcl  42760  relexp01min  42766  corcltrcl  42792  cotrclrcl  42795  frege131d  42817  rnfdmpr  46287  31prm  46563