Theorem uneq12d 3373

Description: Equality deduction for union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Hypotheses

Ref	Expression
uneq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
uneq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
uneq12d	⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

Proof of Theorem uneq12d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		uneq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		uneq12 3367	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

Syntax hints:   → wi 4   = wceq 1398   ∪ cun 3208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-un 3214

This theorem is referenced by:  disjpr2  3752  diftpsn3  3834  iunxprg  4071  undifexmid  4305  exmidundif  4318  exmidundifim  4319  exmid1stab  4320  suceq  4522  rnpropg  5241  fntpg  5411  fresaunres2disj  5544  foun  5632  fnimapr  5736  fprg  5866  fsnunfv  5884  fsnunres  5885  tfrlemi1  6562  tfr1onlemaccex  6578  tfrcllemaccex  6591  ereq1  6773  mapunen  7103  undifdc  7183  unfiin  7185  djueq12  7329  fztp  10411  fzsuc2  10412  fseq1p1m1  10427  ennnfonelemg  13146  ennnfonelemp1  13149  ennnfonelem1  13150  ennnfonelemnn0  13165  setsvalg  13234  setsfun0  13240  setsresg  13242  setsslid  13255  prdsex  13474  prdsval  13478  psrval  14806  lgsquadlem2  15943  vtxdfifiun  16284  trlsegvdegfi  16454