Theorem uneq12 4158

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 4156	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
2		uneq2 4157	. 2 ⊢ (𝐶 = 𝐷 → (𝐵 ∪ 𝐶) = (𝐵 ∪ 𝐷))
3	1, 2	sylan9eq 2793	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∪ cun 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3953

This theorem is referenced by:  uneq12i  4161  uneq12d  4164  un00  4442  opthprc  5739  dmpropg  6212  unixp  6279  fntpg  6606  fnun  6661  resasplit  6759  fvun  6979  rankprb  9843  pm54.43  9993  pwmndgplus  18813  evlseu  21638  ptuncnv  23303  sshjval  30591  bj-2upleq  35882  bj-unexg  35908  poimirlem4  36481  poimirlem9  36486  evlselvlem  41156  diophun  41497  pwssplit4  41817  clsk1indlem3  42780