Theorem uneq2i 2184

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 2181	. 2 ⊢ (A = B → (C ∪ A) = (C ∪ B))
3	1, 2	ax-mp 7	1 ⊢ (C ∪ A) = (C ∪ B)

Syntax hints:   = wceq 958   ∪ cun 2048

This theorem is referenced by:  un23 2192  un4 2193  unundir 2195  difun2 2346  difdifdir 2350  unidif0 2744  unisuc 3052  onuninsuc 3114  fvsnun1 3801  fopabap 3847  tfrlem10 3926  oarec 4202  dfdom2 4390  fodomr 4489  unifiOLD 4570  ranksuc 4710  kmlem3 4777  cda0en 4937  xp2cda 4940  facnnt 6933  fac0 6934

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-un 2053

Copyright terms: Public domain