Theorem uneq12i 4165

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

This proof depends on syntax axioms:   = wceq 1569   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151

This theorem is used by:  indir  4231  difundir  4236  difindi  4237  dfsymdif3  4251  unrab  4260  rabun2  4269  elnelun  4342  dfif6  4484  dfif3  4496  dfif5  4498  symdif0  5044  symdifid  5046  unopab  5184  xpundi  5719  xpundir  5720  xpun  5724  dmun  5891  resundi  5983  resundir  5984  cnvun  6132  rnun  6135  imaundi  6140  imaundir  6141  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  38555  poimirlem19  38558  itg2addnclem2  38591  iblabsnclem  38602  dfproplem  38642  dfsucmap3  39396  redvmptabs  43412  df3o3  44316  rclexi  44615  rtrclex  44617  cnvrcl0  44625  dfrtrcl5  44629  dfrcl2  44674  dfrcl4  44676  iunrelexp0  44702  relexpiidm  44704  corclrcl  44707  relexp01min  44713  corcltrcl  44739  cotrclrcl  44742  frege131d  44764  rnfdmpr  48351  31prm  48682