Theorem uneq12 3985

Description: Equality theorem for the union of two classes. (Contributed by NM, 29-Mar-1998.)

Assertion

Ref	Expression
uneq12	⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

Proof of Theorem uneq12

Step	Hyp	Ref	Expression
1		uneq1 3983	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
2		uneq2 3984	. 2 ⊢ (𝐶 = 𝐷 → (𝐵 ∪ 𝐶) = (𝐵 ∪ 𝐷))
3	1, 2	sylan9eq 2834	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∪ cun 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-un 3797

This theorem is referenced by:  uneq12i  3988  uneq12d  3991  un00  4237  opthprc  5415  dmpropg  5864  unixp  5924  fntpg  6196  fnun  6245  resasplit  6326  fvun  6530  rankprb  9013  pm54.43  9161  xpscg  16615  evlseu  19923  ptuncnv  22030  sshjval  28798  bj-2upleq  33580  poimirlem4  34048  poimirlem9  34053  diophun  38311  pwssplit4  38632  clsk1indlem3  39311