Theorem ifeq2 4505

Description: Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)

Assertion

Ref	Expression
ifeq2	⊢ (𝐴 = 𝐵 → if(𝜑, 𝐶, 𝐴) = if(𝜑, 𝐶, 𝐵))

Proof of Theorem ifeq2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rabeq 3430	. . 3 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} = {𝑥 ∈ 𝐵 ∣ ¬ 𝜑})
2	1	uneq2d 4143	. 2 ⊢ (𝐴 = 𝐵 → ({𝑥 ∈ 𝐶 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) = ({𝑥 ∈ 𝐶 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ ¬ 𝜑}))
3		dfif6 4503	. 2 ⊢ if(𝜑, 𝐶, 𝐴) = ({𝑥 ∈ 𝐶 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑})
4		dfif6 4503	. 2 ⊢ if(𝜑, 𝐶, 𝐵) = ({𝑥 ∈ 𝐶 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ ¬ 𝜑})
5	2, 3, 4	3eqtr4g 2795	1 ⊢ (𝐴 = 𝐵 → if(𝜑, 𝐶, 𝐴) = if(𝜑, 𝐶, 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540  {crab 3415   ∪ cun 3924  ifcif 4500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-un 3931  df-if 4501

This theorem is referenced by:  ifeq12  4519  ifeq2d  4521  ifbieq2i  4526  somincom  6123  mdetunilem9  22558  prmorcht  27140  pclogsum  27178  matunitlindflem1  37640  ftc1anclem6  37722  ftc1anclem8  37724  ftc1anc  37725  hdmap1cbv  41821  reabssgn  43660  hoidmv1le  46623  hoidmvlelem3  46626  vonn0ioo  46716  vonn0icc  46717