Theorem ifeq2 4493

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 3420	. . 3 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} = {𝑥 ∈ 𝐵 ∣ ¬ 𝜑})
2	1	uneq2d 4131	. 2 ⊢ (𝐴 = 𝐵 → ({𝑥 ∈ 𝐶 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) = ({𝑥 ∈ 𝐶 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ ¬ 𝜑}))
3		dfif6 4491	. 2 ⊢ if(𝜑, 𝐶, 𝐴) = ({𝑥 ∈ 𝐶 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑})
4		dfif6 4491	. 2 ⊢ if(𝜑, 𝐶, 𝐵) = ({𝑥 ∈ 𝐶 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ ¬ 𝜑})
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → if(𝜑, 𝐶, 𝐴) = if(𝜑, 𝐶, 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540  {crab 3405   ∪ cun 3912  ifcif 4488

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-un 3919  df-if 4489

This theorem is referenced by:  ifeq12  4507  ifeq2d  4509  ifbieq2i  4514  somincom  6107  mdetunilem9  22507  prmorcht  27088  pclogsum  27126  matunitlindflem1  37610  ftc1anclem6  37692  ftc1anclem8  37694  ftc1anc  37695  hdmap1cbv  41796  reabssgn  43625  hoidmv1le  46592  hoidmvlelem3  46595  vonn0ioo  46685  vonn0icc  46686