Theorem uneq2 4160

Description: Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
uneq2	⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

Proof of Theorem uneq2

Step	Hyp	Ref	Expression
1		uneq1 4159	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
2		uncom 4156	. 2 ⊢ (𝐶 ∪ 𝐴) = (𝐴 ∪ 𝐶)
3		uncom 4156	. 2 ⊢ (𝐶 ∪ 𝐵) = (𝐵 ∪ 𝐶)
4	1, 2, 3	3eqtr4g 2820	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∪ cun 4148

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 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4150

This theorem is used by:  uneq12  4161  uneq2i  4163  uneq2d  4166  uneqin  4233  disjssun  4420  undifixp  8970  unfi  9194  unxpdom  9258  rankung  9880  ackbij1lem16  10319  fin23lem28  10425  ttukeylem6  10599  lcmfun  16829  ipodrsima  18724  mplsubglem  22315  mretopd  23419  iscldtop  23422  dfconn2  23746  nconnsubb  23750  comppfsc  23860  noextendseq  28033  oncutlt  28659  spanun  32156  constrextdg2lem  34430  locfinref  34523  isros  34851  unelros  34854  difelros  34855  rossros  34863  inelcarsg  34993  fineqvac  35852  bj-funun  38310  paddval  40992  dochsatshp  42645  nacsfix  43860  eldioph4b  43955  eldioph4i  43956  fiuneneq  44331  isotone1  45185  fiiuncl  46218