Theorem uneq2i 1608

Description: Inference adding union to the left in a class equality.

Hypothesis

Ref	Expression
uneq1i.1	⊢ A = B

Assertion

Ref	Expression
uneq2i	⊢ (C ∪ A) = (C ∪ B)

Proof of Theorem uneq2i

Step	Hyp	Ref	Expression
1		uneq1i.1	. 2 ⊢ A = B
2		uneq2 1606	. 2 ⊢ (A = B → (C ∪ A) = (C ∪ B))
3	1, 2	ax-mp 6	1 ⊢ (C ∪ A) = (C ∪ B)

Syntax hints:   = wceq 1091   ∪ cun 1485

This theorem is referenced by:  uneq12i 1609  un23 1617  un4 1618  unundir 1620  difun2 1763  difdifdir 1765  unidif0 1944  unisuc 2299  onuninsuc 2356  dfdom2 3288  kmlem3 3582  fodomb 3615  cda0en 3720  xp2cda 3723  facnnt 4870  ruclem7 4891

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-un 1490

metamath.org