![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbceqg | Structured version Visualization version GIF version |
Description: Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Ref | Expression |
---|---|
sbceqg | ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsbcq2 3781 | . . 3 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝐵 = 𝐶 ↔ [𝐴 / 𝑥]𝐵 = 𝐶)) | |
2 | dfsbcq2 3781 | . . . . 5 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑦 ∈ 𝐵)) | |
3 | 2 | abbidv 2802 | . . . 4 ⊢ (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}) |
4 | dfsbcq2 3781 | . . . . 5 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝑦 ∈ 𝐶 ↔ [𝐴 / 𝑥]𝑦 ∈ 𝐶)) | |
5 | 4 | abbidv 2802 | . . . 4 ⊢ (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}) |
6 | 3, 5 | eqeq12d 2749 | . . 3 ⊢ (𝑧 = 𝐴 → ({𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶} ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶})) |
7 | nfs1v 2154 | . . . . . 6 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝑦 ∈ 𝐵 | |
8 | 7 | nfab 2910 | . . . . 5 ⊢ Ⅎ𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} |
9 | nfs1v 2154 | . . . . . 6 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝑦 ∈ 𝐶 | |
10 | 9 | nfab 2910 | . . . . 5 ⊢ Ⅎ𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶} |
11 | 8, 10 | nfeq 2917 | . . . 4 ⊢ Ⅎ𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶} |
12 | sbab 2883 | . . . . 5 ⊢ (𝑥 = 𝑧 → 𝐵 = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵}) | |
13 | sbab 2883 | . . . . 5 ⊢ (𝑥 = 𝑧 → 𝐶 = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶}) | |
14 | 12, 13 | eqeq12d 2749 | . . . 4 ⊢ (𝑥 = 𝑧 → (𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶})) |
15 | 11, 14 | sbiev 2309 | . . 3 ⊢ ([𝑧 / 𝑥]𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶}) |
16 | 1, 6, 15 | vtoclbg 3560 | . 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶})) |
17 | df-csb 3895 | . . 3 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | |
18 | df-csb 3895 | . . 3 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶} | |
19 | 17, 18 | eqeq12i 2751 | . 2 ⊢ (⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶 ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}) |
20 | 16, 19 | bitr4di 289 | 1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 [wsb 2068 ∈ wcel 2107 {cab 2710 [wsbc 3778 ⦋csb 3894 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-sbc 3779 df-csb 3895 |
This theorem is referenced by: sbceqi 4411 sbcne12 4413 sbceq1g 4415 sbceq2g 4417 csbie2df 4441 sbcfng 6715 csbfrecsg 8269 swrdspsleq 14615 fprodmodd 15941 relowlpssretop 36245 rdgeqoa 36251 poimirlem25 36513 cdlemk42 39812 minregex 42285 onfrALTlem5 43303 onfrALTlem4 43304 csbingVD 43645 onfrALTlem5VD 43646 onfrALTlem4VD 43647 csbeq2gVD 43653 csbsngVD 43654 csbunigVD 43659 csbfv12gALTVD 43660 |
Copyright terms: Public domain | W3C validator |