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 2786	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534   ∪ cun 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-un 3952

This theorem is referenced by:  uneq12i  4161  uneq12d  4164  un00  4447  opthprc  5746  dmpropg  6226  unixp  6293  fntpg  6619  fnun  6674  resasplit  6772  fvun  6992  rankprb  9894  pm54.43  10044  pwmndgplus  18925  evlseu  22098  ptuncnv  23802  sshjval  31283  bj-2upleq  36702  bj-unexg  36728  poimirlem4  37308  poimirlem9  37313  evlselvlem  42041  diophun  42413  pwssplit4  42733  clsk1indlem3  43693

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »