Theorem uneq12i 3900

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

Syntax hints:   = wceq 1624   ∪ cun 3705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334  df-un 3712

This theorem is referenced by:  indir  4010  difundir  4015  difindi  4016  dfsymdif3  4028  unrab  4033  rabun2  4041  elnelun  4099  elnelunOLD  4101  dfif6  4225  dfif3  4236  dfif5  4238  symdif0  4741  symdifid  4743  unopab  4872  xpundi  5320  xpundir  5321  xpun  5325  dmun  5478  resundi  5560  resundir  5561  cnvun  5688  rnun  5691  imaundi  5695  imaundir  5696  dmtpop  5762  coundi  5789  coundir  5790  unidmrn  5818  dfdm2  5820  predun  5857  mptun  6178  resasplit  6227  fresaun  6228  fresaunres2  6229  residpr  6564  fpr  6576  fvsnun2  6605  sbthlem5  8231  1sdom  8320  cdaassen  9188  fz0to3un2pr  12627  fz0to4untppr  12628  fzo0to42pr  12741  hashgval  13306  hashinf  13308  relexpcnv  13966  bpoly3  14980  vdwlem6  15884  setsres  16095  xpsc  16411  lefld  17419  opsrtoslem1  19678  volun  23505  iblcnlem1  23745  ex-dif  27583  ex-in  27585  ex-pw  27589  ex-xp  27596  ex-cnv  27597  ex-rn  27600  partfun  29776  ordtprsuni  30266  indval2  30377  sigaclfu2  30485  eulerpartgbij  30735  subfacp1lem1  31460  subfacp1lem5  31465  fixun  32314  refssfne  32651  onint1  32746  bj-pr1un  33289  bj-pr21val  33299  bj-pr2un  33303  bj-pr22val  33305  poimirlem16  33730  poimirlem19  33733  itg2addnclem2  33767  iblabsnclem  33778  rclexi  38416  rtrclex  38418  cnvrcl0  38426  dfrtrcl5  38430  dfrcl2  38460  dfrcl4  38462  iunrelexp0  38488  relexpiidm  38490  corclrcl  38493  relexp01min  38499  corcltrcl  38525  cotrclrcl  38528  frege131d  38550  df3o3  38817  rnfdmpr  41800  31prm  42014