![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ifeq1 | Structured version Visualization version GIF version |
Description: Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Ref | Expression |
---|---|
ifeq1 | ⊢ (𝐴 = 𝐵 → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabeq 3448 | . . 3 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) | |
2 | 1 | uneq1d 4177 | . 2 ⊢ (𝐴 = 𝐵 → ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐶 ∣ ¬ 𝜑}) = ({𝑥 ∈ 𝐵 ∣ 𝜑} ∪ {𝑥 ∈ 𝐶 ∣ ¬ 𝜑})) |
3 | dfif6 4534 | . 2 ⊢ if(𝜑, 𝐴, 𝐶) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐶 ∣ ¬ 𝜑}) | |
4 | dfif6 4534 | . 2 ⊢ if(𝜑, 𝐵, 𝐶) = ({𝑥 ∈ 𝐵 ∣ 𝜑} ∪ {𝑥 ∈ 𝐶 ∣ ¬ 𝜑}) | |
5 | 2, 3, 4 | 3eqtr4g 2800 | 1 ⊢ (𝐴 = 𝐵 → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1537 {crab 3433 ∪ cun 3961 ifcif 4531 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-rab 3434 df-v 3480 df-un 3968 df-if 4532 |
This theorem is referenced by: ifeq12 4549 ifeq1d 4550 ifbieq12i 4558 rdgeq2 8451 dfoi 9549 wemaplem2 9585 cantnflem1 9727 prodeq2w 15943 prodeq2ii 15944 mgm2nsgrplem2 18945 mgm2nsgrplem3 18946 mplcoe3 22074 marrepval0 22583 ellimc 25923 ply1nzb 26177 dchrvmasumiflem1 27560 signspval 34546 dfrdg2 35777 sumeq2si 36184 prodeq2si 36186 dfafv22 47209 |
Copyright terms: Public domain | W3C validator |