Theorem uneq12 4173

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∪ cun 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968

This theorem is referenced by:  uneq12i  4176  uneq12d  4179  un00  4451  opthprc  5753  dmpropg  6237  unixp  6304  fntpg  6628  fnun  6683  resasplit  6779  fvun  6999  rankprb  9889  pm54.43  10039  pwmndgplus  18961  evlseu  22125  ptuncnv  23831  sshjval  31379  bj-2upleq  36995  bj-unexg  37021  poimirlem4  37611  poimirlem9  37616  evlselvlem  42573  diophun  42761  pwssplit4  43078  clsk1indlem3  44033