Theorem uneq12i 4113

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

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904

This theorem is used by:  indir  4232  difundir  4237  difindi  4238  dfsymdif3  4252  unrab  4261  rabun2  4270  elnelun  4343  dfif6  4485  dfif3  4497  dfif5  4499  symdif0  5045  symdifid  5047  unopab  5185  xpundi  5720  xpundir  5721  xpun  5725  dmun  5892  resundi  5984  resundir  5985  cnvun  6133  rnun  6136  imaundi  6141  imaundir  6142  dmtpop  6219  coundi  6248  coundir  6249  unidmrn  6282  dfdm2  6284  predun  6331  mptun  6685  partfun  6686  resasplit  6752  fresaun  6753  fresaunres2  6754  residpr  7146  fpr  7158  sbthlem5  9110  djuassen  10257  indval2  12325  indconst0  12332  fz0to3un2pr  13763  fz0to4untppr  13764  fz0to5un2tp  13765  fzo0to42pr  13888  hashgval  14477  hashinf  14479  relexpcnv  15188  bpoly3  16224  vdwlem6  17164  setsres  17356  lefld  18766  opsrtoslem1  22364  volun  25866  nosupcbv  28059  noinfcbv  28074  lrold  28283  addsval2  28349  addcuts  28364  addsunif  28388  addbday  28404  mulsval2  28497  muls01  28498  mulsproplem2  28503  mulsproplem3  28504  mulsproplem4  28505  mulcut  28518  mulsunif  28536  addsdilem1  28537  addsdilem2  28538  mulsasslem1  28549  mulsasslem2  28550  mulsunif2  28556  precsexlemcbv  28592  onaddscl  28663  onmulscl  28664  n0cut  28720  twocut  28809  bdaypw2n0bndlem  28849  0reno  28882  1reno  28883  ex-dif  31024  ex-in  31026  ex-pw  31030  ex-xp  31037  ex-cnv  31038  ex-rn  31041  fzodif1  33384  ordtprsuni  34551  sigaclfu2  34753  eulerpartgbij  35004  subfacp1lem1  35944  subfacp1lem5  35949  fmla1  36152  fixun  36671  refssfne  37146  onint1  37237  ttcun  37300  bj-pr1un  37916  bj-pr21val  37926  bj-pr2un  37930  bj-pr22val  37932  poimirlem16  38554  poimirlem19  38557  itg2addnclem2  38590  iblabsnclem  38601  dfproplem  38641  dfsucmap3  39395  redvmptabs  43411  df3o3  44315  rclexi  44614  rtrclex  44616  cnvrcl0  44624  dfrtrcl5  44628  dfrcl2  44673  dfrcl4  44675  iunrelexp0  44701  relexpiidm  44703  corclrcl  44706  relexp01min  44712  corcltrcl  44738  cotrclrcl  44741  frege131d  44763  rnfdmpr  48350  31prm  48681