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 3483 | . . 3 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) | |
2 | 1 | uneq1d 4138 | . 2 ⊢ (𝐴 = 𝐵 → ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐶 ∣ ¬ 𝜑}) = ({𝑥 ∈ 𝐵 ∣ 𝜑} ∪ {𝑥 ∈ 𝐶 ∣ ¬ 𝜑})) |
3 | dfif6 4470 | . 2 ⊢ if(𝜑, 𝐴, 𝐶) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐶 ∣ ¬ 𝜑}) | |
4 | dfif6 4470 | . 2 ⊢ if(𝜑, 𝐵, 𝐶) = ({𝑥 ∈ 𝐵 ∣ 𝜑} ∪ {𝑥 ∈ 𝐶 ∣ ¬ 𝜑}) | |
5 | 2, 3, 4 | 3eqtr4g 2881 | 1 ⊢ (𝐴 = 𝐵 → if(𝜑, 𝐴, 𝐶) = if(𝜑, 𝐵, 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1537 {crab 3142 ∪ cun 3934 ifcif 4467 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-un 3941 df-if 4468 |
This theorem is referenced by: ifeq12 4484 ifeq1d 4485 ifbieq12i 4493 rdgeq2 8048 dfoi 8975 wemaplem2 9011 cantnflem1 9152 prodeq2w 15266 prodeq2ii 15267 mgm2nsgrplem2 18084 mgm2nsgrplem3 18085 mplcoe3 20247 marrepval0 21170 ellimc 24471 ply1nzb 24716 dchrvmasumiflem1 26077 signspval 31822 dfrdg2 33040 dfafv22 43478 |
Copyright terms: Public domain | W3C validator |