Theorem uneq12i 3765

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

Syntax hints:   = wceq 1483   ∪ cun 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579

This theorem is referenced by:  indir  3875  difundir  3880  difindi  3881  dfsymdif3  3893  unrab  3898  rabun2  3906  elnelun  3964  elnelunOLD  3966  dfif6  4089  dfif3  4100  dfif5  4102  symdif0  4597  symdifid  4599  unopab  4728  xpundi  5171  xpundir  5172  xpun  5176  dmun  5331  resundi  5410  resundir  5411  cnvun  5538  rnun  5541  imaundi  5545  imaundir  5546  dmtpop  5611  coundi  5636  coundir  5637  unidmrn  5665  dfdm2  5667  predun  5704  mptun  6025  resasplit  6074  fresaun  6075  fresaunres2  6076  residpr  6409  fpr  6421  fvsnun2  6449  sbthlem5  8074  1sdom  8163  cdaassen  9004  fz0to3un2pr  12441  fz0to4untppr  12442  fzo0to42pr  12555  hashgval  13120  hashinf  13122  relexpcnv  13775  bpoly3  14789  vdwlem6  15690  setsres  15901  xpsc  16217  lefld  17226  opsrtoslem1  19484  volun  23313  iblcnlem1  23554  ex-dif  27280  ex-in  27282  ex-pw  27286  ex-xp  27293  ex-cnv  27294  ex-rn  27297  partfun  29475  ordtprsuni  29965  indval2  30076  sigaclfu2  30184  eulerpartgbij  30434  subfacp1lem1  31161  subfacp1lem5  31166  fixun  32016  refssfne  32353  onint1  32448  bj-pr1un  32991  bj-pr21val  33001  bj-pr2un  33005  bj-pr22val  33007  poimirlem16  33425  poimirlem19  33428  itg2addnclem2  33462  iblabsnclem  33473  rclexi  37922  rtrclex  37924  cnvrcl0  37932  dfrtrcl5  37936  dfrcl2  37966  dfrcl4  37968  iunrelexp0  37994  relexpiidm  37996  corclrcl  37999  relexp01min  38005  corcltrcl  38031  cotrclrcl  38034  frege131d  38056  df3o3  38323  rnfdmpr  41300  31prm  41512