Theorem uneq12i 4106

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

Syntax hints:   = wceq 1540   ∪ cun 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-un 3902

This theorem is referenced by:  indir  4220  difundir  4225  difindi  4226  dfsymdif3  4241  unrab  4250  rabun2  4258  elnelun  4334  dfif6  4474  dfif3  4485  dfif5  4487  symdif0  5027  symdifid  5029  unopab  5169  xpundi  5673  xpundir  5674  xpun  5678  dmun  5839  resundi  5924  resundir  5925  cnvun  6068  rnun  6071  imaundi  6075  imaundir  6076  dmtpop  6143  coundi  6172  coundir  6173  unidmrn  6204  dfdm2  6206  predun  6253  mptun  6616  partfun  6617  resasplit  6681  fresaun  6682  fresaunres2  6683  residpr  7054  fpr  7065  sbthlem5  8929  1sdomOLD  9091  djuassen  10007  fz0to3un2pr  13431  fz0to4untppr  13432  fzo0to42pr  13547  hashgval  14120  hashinf  14122  relexpcnv  14818  bpoly3  15840  vdwlem6  16757  setsres  16949  lefld  18380  opsrtoslem1  21334  volun  24781  ex-dif  28896  ex-in  28898  ex-pw  28902  ex-xp  28909  ex-cnv  28910  ex-rn  28913  fzodif1  31222  ordtprsuni  31975  indval2  32088  sigaclfu2  32195  eulerpartgbij  32445  subfacp1lem1  33246  subfacp1lem5  33251  fmla1  33454  nosupcbv  33963  noinfcbv  33978  lrold  34135  fixun  34269  refssfne  34605  onint1  34696  bj-pr1un  35249  bj-pr21val  35259  bj-pr2un  35263  bj-pr22val  35265  poimirlem16  35849  poimirlem19  35852  itg2addnclem2  35885  iblabsnclem  35896  rclexi  41444  rtrclex  41446  cnvrcl0  41454  dfrtrcl5  41458  dfrcl2  41503  dfrcl4  41505  iunrelexp0  41531  relexpiidm  41533  corclrcl  41536  relexp01min  41542  corcltrcl  41568  cotrclrcl  41571  frege131d  41593  df3o3  41856  rnfdmpr  45025  31prm  45301