Theorem uneq12i 3743

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

Syntax hints:   = wceq 1480   ∪ cun 3553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-un 3560

This theorem is referenced by:  indir  3851  difundir  3856  difindi  3857  dfsymdif3  3869  unrab  3874  rabun2  3882  elnelun  3938  dfif6  4061  dfif3  4072  dfif5  4074  symdif0  4563  symdifid  4565  unopab  4690  xpundi  5132  xpundir  5133  xpun  5137  dmun  5291  resundi  5369  resundir  5370  cnvun  5497  rnun  5500  imaundi  5504  imaundir  5505  dmtpop  5570  coundi  5595  coundir  5596  unidmrn  5624  dfdm2  5626  predun  5663  mptun  5982  resasplit  6031  fresaun  6032  fresaunres2  6033  residpr  6363  fpr  6375  fvsnun2  6403  sbthlem5  8018  1sdom  8107  cdaassen  8948  fz0to3un2pr  12382  fz0to4untppr  12383  fzo0to42pr  12496  hashgval  13060  hashinf  13062  relexpcnv  13709  bpoly3  14714  vdwlem6  15614  setsres  15822  xpsc  16138  lefld  17147  opsrtoslem1  19403  volun  23220  iblcnlem1  23460  ex-dif  27134  ex-in  27136  ex-pw  27140  ex-xp  27147  ex-cnv  27148  ex-rn  27151  partfun  29318  ordtprsuni  29747  indval2  29858  sigaclfu2  29965  eulerpartgbij  30215  subfacp1lem1  30869  subfacp1lem5  30874  fixun  31658  refssfne  31995  onint1  32090  bj-pr1un  32638  bj-pr21val  32648  bj-pr2un  32652  bj-pr22val  32654  poimirlem16  33057  poimirlem19  33060  itg2addnclem2  33094  iblabsnclem  33105  rclexi  37403  rtrclex  37405  cnvrcl0  37413  dfrtrcl5  37417  dfrcl2  37447  dfrcl4  37449  iunrelexp0  37475  relexpiidm  37477  corclrcl  37480  relexp01min  37486  corcltrcl  37512  cotrclrcl  37515  frege131d  37537  df3o3  37805  rnfdmpr  40597  31prm  40811