Theorem uneq12i 4095

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

Syntax hints:   = wceq 1539   ∪ cun 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892

This theorem is referenced by:  indir  4209  difundir  4214  difindi  4215  dfsymdif3  4230  unrab  4239  rabun2  4247  elnelun  4323  dfif6  4462  dfif3  4473  dfif5  4475  symdif0  5014  symdifid  5016  unopab  5156  xpundi  5655  xpundir  5656  xpun  5660  dmun  5819  resundi  5905  resundir  5906  cnvun  6046  rnun  6049  imaundi  6053  imaundir  6054  dmtpop  6121  coundi  6151  coundir  6152  unidmrn  6182  dfdm2  6184  predun  6231  mptun  6579  partfun  6580  resasplit  6644  fresaun  6645  fresaunres2  6646  residpr  7015  fpr  7026  sbthlem5  8874  1sdom  9025  djuassen  9934  fz0to3un2pr  13358  fz0to4untppr  13359  fzo0to42pr  13474  hashgval  14047  hashinf  14049  relexpcnv  14746  bpoly3  15768  vdwlem6  16687  setsres  16879  lefld  18310  opsrtoslem1  21262  volun  24709  ex-dif  28787  ex-in  28789  ex-pw  28793  ex-xp  28800  ex-cnv  28801  ex-rn  28804  fzodif1  31114  ordtprsuni  31869  indval2  31982  sigaclfu2  32089  eulerpartgbij  32339  subfacp1lem1  33141  subfacp1lem5  33146  fmla1  33349  nosupcbv  33905  noinfcbv  33920  lrold  34077  fixun  34211  refssfne  34547  onint1  34638  bj-pr1un  35193  bj-pr21val  35203  bj-pr2un  35207  bj-pr22val  35209  poimirlem16  35793  poimirlem19  35796  itg2addnclem2  35829  iblabsnclem  35840  rclexi  41223  rtrclex  41225  cnvrcl0  41233  dfrtrcl5  41237  dfrcl2  41282  dfrcl4  41284  iunrelexp0  41310  relexpiidm  41312  corclrcl  41315  relexp01min  41321  corcltrcl  41347  cotrclrcl  41350  frege131d  41372  df3o3  41635  rnfdmpr  44773  31prm  45049