Theorem ifeq2 4481

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540  {crab 3394   ∪ cun 3901  ifcif 4476

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 3395  df-v 3438  df-un 3908  df-if 4477

This theorem is referenced by:  ifeq12  4495  ifeq2d  4497  ifbieq2i  4502  somincom  6083  mdetunilem9  22505  prmorcht  27086  pclogsum  27124  matunitlindflem1  37600  ftc1anclem6  37682  ftc1anclem8  37684  ftc1anc  37685  hdmap1cbv  41785  reabssgn  43613  hoidmv1le  46579  hoidmvlelem3  46582  vonn0ioo  46672  vonn0icc  46673