Theorem uneq12i 4091

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

Syntax hints:   = wceq 1539   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888

This theorem is referenced by:  indir  4206  difundir  4211  difindi  4212  dfsymdif3  4227  unrab  4236  rabun2  4244  elnelun  4320  dfif6  4459  dfif3  4470  dfif5  4472  symdif0  5010  symdifid  5012  unopab  5152  xpundi  5646  xpundir  5647  xpun  5651  dmun  5808  resundi  5894  resundir  5895  cnvun  6035  rnun  6038  imaundi  6042  imaundir  6043  dmtpop  6110  coundi  6140  coundir  6141  unidmrn  6171  dfdm2  6173  predun  6220  mptun  6563  partfun  6564  resasplit  6628  fresaun  6629  fresaunres2  6630  residpr  6997  fpr  7008  sbthlem5  8827  1sdom  8955  djuassen  9865  fz0to3un2pr  13287  fz0to4untppr  13288  fzo0to42pr  13402  hashgval  13975  hashinf  13977  relexpcnv  14674  bpoly3  15696  vdwlem6  16615  setsres  16807  lefld  18225  opsrtoslem1  21172  volun  24614  ex-dif  28688  ex-in  28690  ex-pw  28694  ex-xp  28701  ex-cnv  28702  ex-rn  28705  fzodif1  31016  ordtprsuni  31771  indval2  31882  sigaclfu2  31989  eulerpartgbij  32239  subfacp1lem1  33041  subfacp1lem5  33046  fmla1  33249  nosupcbv  33832  noinfcbv  33847  lrold  34004  fixun  34138  refssfne  34474  onint1  34565  bj-pr1un  35120  bj-pr21val  35130  bj-pr2un  35134  bj-pr22val  35136  poimirlem16  35720  poimirlem19  35723  itg2addnclem2  35756  iblabsnclem  35767  rclexi  41112  rtrclex  41114  cnvrcl0  41122  dfrtrcl5  41126  dfrcl2  41171  dfrcl4  41173  iunrelexp0  41199  relexpiidm  41201  corclrcl  41204  relexp01min  41210  corcltrcl  41236  cotrclrcl  41239  frege131d  41261  df3o3  41524  rnfdmpr  44660  31prm  44937