Theorem uneq2 4096

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 4095	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
2		uncom 4092	. 2 ⊢ (𝐶 ∪ 𝐴) = (𝐴 ∪ 𝐶)
3		uncom 4092	. 2 ⊢ (𝐶 ∪ 𝐵) = (𝐵 ∪ 𝐶)
4	1, 2, 3	3eqtr4g 2805	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-un 3897

This theorem is referenced by:  uneq12  4097  uneq2i  4099  uneq2d  4102  uneqin  4218  disjssun  4407  uniprgOLD  4865  unexb  7590  undifixp  8697  unfi  8929  unxpdom  9000  ackbij1lem16  9984  fin23lem28  10089  ttukeylem6  10263  lcmfun  16340  ipodrsima  18249  mplsubglem  21195  mretopd  22233  iscldtop  22236  dfconn2  22560  nconnsubb  22564  comppfsc  22673  spanun  29895  locfinref  31779  isros  32124  unelros  32127  difelros  32128  rossros  32136  inelcarsg  32266  fineqvac  33054  noextendseq  33858  rankung  34456  bj-funun  35411  paddval  37800  dochsatshp  39453  nacsfix  40523  eldioph4b  40622  eldioph4i  40623  fiuneneq  41011  isotone1  41620  fiiuncl  42575