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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  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  5724  xpundir  5725  xpun  5729  dmun  5894  resundi  5986  resundir  5987  cnvun  6133  rnun  6136  imaundi  6141  imaundir  6142  dmtpop  6214  coundi  6243  coundir  6244  unidmrn  6277  dfdm2  6279  predun  6326  mptun  6679  partfun  6680  resasplit  6746  fresaun  6747  fresaunres2  6748  residpr  7140  fpr  7152  sbthlem5  9092  djuassen  10184  indval2  12250  indconst0  12257  fz0to3un2pr  13687  fz0to4untppr  13688  fz0to5un2tp  13689  fzo0to42pr  13812  hashgval  14400  hashinf  14402  relexpcnv  15111  bpoly3  16147  vdwlem6  17081  setsres  17273  lefld  18683  opsrtoslem1  22274  volun  25776  nosupcbv  27941  noinfcbv  27956  lrold  28165  addsval2  28231  addcuts  28246  addsunif  28270  addbday  28286  mulsval2  28379  muls01  28380  mulsproplem2  28385  mulsproplem3  28386  mulsproplem4  28387  mulcut  28400  mulsunif  28418  addsdilem1  28419  addsdilem2  28420  mulsasslem1  28431  mulsasslem2  28432  mulsunif2  28438  precsexlemcbv  28474  onaddscl  28545  onmulscl  28546  n0cut  28602  twocut  28691  bdaypw2n0bndlem  28731  0reno  28764  1reno  28765  ex-dif  30906  ex-in  30908  ex-pw  30912  ex-xp  30919  ex-cnv  30920  ex-rn  30923  fzodif1  33266  ordtprsuni  34432  sigaclfu2  34634  eulerpartgbij  34886  subfacp1lem1  35761  subfacp1lem5  35766  fmla1  35969  fixun  36489  refssfne  36980  onint1  37071  ttcun  37134  bj-pr1un  37750  bj-pr21val  37760  bj-pr2un  37764  bj-pr22val  37766  poimirlem16  38388  poimirlem19  38391  itg2addnclem2  38424  iblabsnclem  38435  dfsucmap3  39214  redvmptabs  43238  df3o3  44158  rclexi  44458  rtrclex  44460  cnvrcl0  44468  dfrtrcl5  44472  dfrcl2  44517  dfrcl4  44519  iunrelexp0  44545  relexpiidm  44547  corclrcl  44550  relexp01min  44556  corcltrcl  44582  cotrclrcl  44585  frege131d  44607  rnfdmpr  48172  31prm  48503