Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbceqg | Structured version Visualization version Unicode 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 3438 | . . 3 | |
2 | dfsbcq2 3438 | . . . . 5 | |
3 | 2 | abbidv 2741 | . . . 4 |
4 | dfsbcq2 3438 | . . . . 5 | |
5 | 4 | abbidv 2741 | . . . 4 |
6 | 3, 5 | eqeq12d 2637 | . . 3 |
7 | nfs1v 2437 | . . . . . 6 | |
8 | 7 | nfab 2769 | . . . . 5 |
9 | nfs1v 2437 | . . . . . 6 | |
10 | 9 | nfab 2769 | . . . . 5 |
11 | 8, 10 | nfeq 2776 | . . . 4 |
12 | sbab 2750 | . . . . 5 | |
13 | sbab 2750 | . . . . 5 | |
14 | 12, 13 | eqeq12d 2637 | . . . 4 |
15 | 11, 14 | sbie 2408 | . . 3 |
16 | 1, 6, 15 | vtoclbg 3267 | . 2 |
17 | df-csb 3534 | . . 3 | |
18 | df-csb 3534 | . . 3 | |
19 | 17, 18 | eqeq12i 2636 | . 2 |
20 | 16, 19 | syl6bbr 278 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wceq 1483 wsb 1880 wcel 1990 cab 2608 wsbc 3435 csb 3533 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-sbc 3436 df-csb 3534 |
This theorem is referenced by: sbcne12 3986 sbceq1g 3988 sbceq2g 3990 sbcfng 6042 swrdspsleq 13449 fprodmodd 14728 csbwrecsg 33173 relowlpssretop 33212 rdgeqoa 33218 poimirlem25 33434 sbceqi 33913 cdlemk42 36229 onfrALTlem5 38757 onfrALTlem4 38758 csbeq2gOLD 38765 csbfv12gALTOLD 39052 csbingVD 39120 onfrALTlem5VD 39121 onfrALTlem4VD 39122 csbeq2gVD 39128 csbsngVD 39129 csbunigVD 39134 csbfv12gALTVD 39135 |
Copyright terms: Public domain | W3C validator |