Theorem uneq12i 4137

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

Syntax hints:   = wceq 1537   ∪ cun 3934

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941

This theorem is referenced by:  indir  4252  difundir  4257  difindi  4258  dfsymdif3  4269  unrab  4274  rabun2  4282  elnelun  4343  dfif6  4470  dfif3  4481  dfif5  4483  symdif0  5007  symdifid  5009  unopab  5145  xpundi  5620  xpundir  5621  xpun  5625  dmun  5779  resundi  5867  resundir  5868  cnvun  6001  rnun  6004  imaundi  6008  imaundir  6009  dmtpop  6075  coundi  6100  coundir  6101  unidmrn  6130  dfdm2  6132  predun  6172  mptun  6494  resasplit  6548  fresaun  6549  fresaunres2  6550  residpr  6905  fpr  6916  sbthlem5  8631  1sdom  8721  djuassen  9604  fz0to3un2pr  13010  fz0to4untppr  13011  fzo0to42pr  13125  hashgval  13694  hashinf  13696  relexpcnv  14394  bpoly3  15412  vdwlem6  16322  setsres  16525  lefld  17836  opsrtoslem1  20264  volun  24146  ex-dif  28202  ex-in  28204  ex-pw  28208  ex-xp  28215  ex-cnv  28216  ex-rn  28219  partfun  30421  fzodif1  30516  ordtprsuni  31162  indval2  31273  sigaclfu2  31380  eulerpartgbij  31630  subfacp1lem1  32426  subfacp1lem5  32431  fmla1  32634  fixun  33370  refssfne  33706  onint1  33797  bj-pr1un  34318  bj-pr21val  34328  bj-pr2un  34332  bj-pr22val  34334  poimirlem16  34923  poimirlem19  34926  itg2addnclem2  34959  iblabsnclem  34970  rclexi  39995  rtrclex  39997  cnvrcl0  40005  dfrtrcl5  40009  dfrcl2  40039  dfrcl4  40041  iunrelexp0  40067  relexpiidm  40069  corclrcl  40072  relexp01min  40078  corcltrcl  40104  cotrclrcl  40107  frege131d  40129  df3o3  40395  rnfdmpr  43500  31prm  43780