Theorem uneq12 4164

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∪ cun 4151

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-un 4153

This theorem is used by:  uneq12i  4167  uneq12d  4170  un00  4359  opthprc  5718  dmpropg  6222  unixp  6291  fntpg  6608  fnun  6661  resasplit  6760  fvun  6983  rankprb  9875  pm54.43  10092  pwmndgplus  19153  evlseu  22404  ptuncnv  24138  sshjval  31964  bj-2upleq  38052  bj-unexg  38078  poimirlem4  38682  poimirlem9  38687  evlselvlem  43756  diophun  43924  pwssplit4  44231  clsk1indlem3  45183