Theorem uneq12d 3309

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 3303	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

Syntax hints:   → wi 4   = wceq 1364   ∪ cun 3146

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2758  df-un 3152

This theorem is referenced by:  disjpr2  3678  diftpsn3  3755  iunxprg  3989  undifexmid  4218  exmidundif  4231  exmidundifim  4232  exmid1stab  4233  suceq  4427  rnpropg  5133  fntpg  5298  foun  5506  fnimapr  5604  fprg  5727  fsnunfv  5745  fsnunres  5746  tfrlemi1  6365  tfr1onlemaccex  6381  tfrcllemaccex  6394  ereq1  6574  undifdc  6960  unfiin  6962  djueq12  7077  fztp  10120  fzsuc2  10121  fseq1p1m1  10136  ennnfonelemg  12471  ennnfonelemp1  12474  ennnfonelem1  12475  ennnfonelemnn0  12490  setsvalg  12559  setsfun0  12565  setsresg  12567  setsslid  12580  prdsex  12791  psrval  14005