Theorem ifeq1 4504

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

Assertion

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

Proof of Theorem ifeq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rabeq 3430	. . 3 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑})
2	1	uneq1d 4142	. 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  ifeq1d  4520  ifbieq12i  4528  rdgeq2  8426  dfoi  9525  wemaplem2  9561  cantnflem1  9703  prodeq2w  15926  prodeq2ii  15927  mgm2nsgrplem2  18897  mgm2nsgrplem3  18898  mplcoe3  21996  marrepval0  22499  ellimc  25826  ply1nzb  26080  dchrvmasumiflem1  27464  signspval  34584  dfrdg2  35813  sumeq2si  36220  prodeq2si  36222  dfafv22  47288