Theorem uneq12i 3613

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

Syntax hints:   = wceq 1468   ∪ cun 3424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485

This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-v 3068  df-un 3431

This theorem is referenced by:  indir  3718  difundir  3723  difindi  3724  dfsymdif3  3735  unrab  3740  rabun2  3748  elnelun  3796  dfif6  3911  dfif3  3922  dfif5  3924  symdif0  4384  symdifid  4386  unopab  4510  xpundi  4934  xpundir  4935  xpun  4939  dmun  5090  resundi  5167  resundir  5168  cnvun  5291  rnun  5294  imaundi  5298  imaundir  5299  dmtpop  5363  coundi  5387  coundir  5388  unidmrn  5417  dfdm2  5419  predun  5455  mptun  5764  resasplit  5811  fresaun  5812  fresaunres2  5813  residpr  6136  fpr  6140  fvsnun2  6168  sbthlem5  7770  1sdom  7859  cdaassen  8697  fz0to3un2pr  11993  fzo0to42pr  12104  hashgval  12632  hashinf  12634  relexpcnv  13258  bpoly3  14271  vdwlem6  15098  setsres  15316  xpsc  15628  lefld  16637  opsrtoslem1  18866  volun  22658  iblcnlem1  22906  usgraexmplvtxlem  25283  ex-dif  26033  ex-in  26035  ex-pw  26039  ex-xp  26046  ex-cnv  26047  ex-rn  26050  partfun  28435  ordtprsuni  28880  indval2  28991  sigaclfu2  29098  eulerpartgbij  29359  subfacp1lem1  30054  subfacp1lem5  30059  fixun  30827  refssfne  31163  onint1  31258  bj-pr1un  31783  bj-pr21val  31793  bj-pr2un  31797  bj-pr22val  31799  poimirlem16  32194  poimirlem19  32197  itg2addnclem2  32232  iblabsnclem  32243  rclexi  36461  rtrclex  36463  cnvrcl0  36471  dfrtrcl5  36475  dfrcl2  36505  dfrcl4  36507  iunrelexp0  36533  relexpiidm  36535  corclrcl  36538  relexp01min  36544  corcltrcl  36570  cotrclrcl  36573  frege131d  36595  rnfdmpr  39536