Theorem uneq12d 3315

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

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

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 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158

This theorem is referenced by:  disjpr2  3683  diftpsn3  3760  iunxprg  3994  undifexmid  4223  exmidundif  4236  exmidundifim  4237  exmid1stab  4238  suceq  4434  rnpropg  5146  fntpg  5311  foun  5520  fnimapr  5618  fprg  5742  fsnunfv  5760  fsnunres  5761  tfrlemi1  6387  tfr1onlemaccex  6403  tfrcllemaccex  6416  ereq1  6596  undifdc  6982  unfiin  6984  djueq12  7100  fztp  10147  fzsuc2  10148  fseq1p1m1  10163  ennnfonelemg  12563  ennnfonelemp1  12566  ennnfonelem1  12567  ennnfonelemnn0  12582  setsvalg  12651  setsfun0  12657  setsresg  12659  setsslid  12672  prdsex  12883  psrval  14163  lgsquadlem2  15235