![]() |
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 2797 | . . . 4 ⊢ (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}) |
4 | dfsbcq2 3781 | . . . . 5 ⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝑦 ∈ 𝐶 ↔ [𝐴 / 𝑥]𝑦 ∈ 𝐶)) | |
5 | 4 | abbidv 2797 | . . . 4 ⊢ (𝑧 = 𝐴 → {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}) |
6 | 3, 5 | eqeq12d 2744 | . . 3 ⊢ (𝑧 = 𝐴 → ({𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶} ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶})) |
7 | nfs1v 2145 | . . . . . 6 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝑦 ∈ 𝐵 | |
8 | 7 | nfab 2905 | . . . . 5 ⊢ Ⅎ𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} |
9 | nfs1v 2145 | . . . . . 6 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝑦 ∈ 𝐶 | |
10 | 9 | nfab 2905 | . . . . 5 ⊢ Ⅎ𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶} |
11 | 8, 10 | nfeq 2913 | . . . 4 ⊢ Ⅎ𝑥{𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶} |
12 | sbab 2878 | . . . . 5 ⊢ (𝑥 = 𝑧 → 𝐵 = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵}) | |
13 | sbab 2878 | . . . . 5 ⊢ (𝑥 = 𝑧 → 𝐶 = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶}) | |
14 | 12, 13 | eqeq12d 2744 | . . . 4 ⊢ (𝑥 = 𝑧 → (𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶})) |
15 | 11, 14 | sbiev 2303 | . . 3 ⊢ ([𝑧 / 𝑥]𝐵 = 𝐶 ↔ {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝑧 / 𝑥]𝑦 ∈ 𝐶}) |
16 | 1, 6, 15 | vtoclbg 3544 | . 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶})) |
17 | df-csb 3895 | . . 3 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | |
18 | df-csb 3895 | . . 3 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶} | |
19 | 17, 18 | eqeq12i 2746 | . 2 ⊢ (⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶 ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}) |
20 | 16, 19 | bitr4di 288 | 1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1533 [wsb 2059 ∈ wcel 2098 {cab 2705 [wsbc 3778 ⦋csb 3894 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1536 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-sbc 3779 df-csb 3895 |
This theorem is referenced by: sbceqi 4414 sbcne12 4416 sbceq1g 4418 sbceq2g 4420 csbie2df 4444 sbcfng 6724 csbfrecsg 8296 swrdspsleq 14655 fprodmodd 15981 relowlpssretop 36876 rdgeqoa 36882 poimirlem25 37151 cdlemk42 40446 minregex 42995 onfrALTlem5 44012 onfrALTlem4 44013 csbingVD 44354 onfrALTlem5VD 44355 onfrALTlem4VD 44356 csbeq2gVD 44362 csbsngVD 44363 csbunigVD 44368 csbfv12gALTVD 44369 |
Copyright terms: Public domain | W3C validator |