Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbie | Structured version Visualization version Unicode version |
Description: Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) |
Ref | Expression |
---|---|
sbie.1 | |
sbie.2 |
Ref | Expression |
---|---|
sbie |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equsb1 2368 | . . 3 | |
2 | sbie.2 | . . . 4 | |
3 | 2 | sbimi 1886 | . . 3 |
4 | 1, 3 | ax-mp 5 | . 2 |
5 | sbie.1 | . . . 4 | |
6 | 5 | sbf 2380 | . . 3 |
7 | 6 | sblbis 2404 | . 2 |
8 | 4, 7 | mpbi 220 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wnf 1708 wsb 1880 |
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-10 2019 ax-12 2047 ax-13 2246 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-ex 1705 df-nf 1710 df-sb 1881 |
This theorem is referenced by: sbied 2409 equsb3lem 2431 elsb3 2434 elsb4 2435 cbveu 2505 mo4f 2516 2mos 2552 eqsb3lem 2727 clelsb3 2729 cbvab 2746 clelsb3f 2768 cbvralf 3165 cbvreu 3169 sbralie 3184 cbvrab 3198 reu2 3394 nfcdeq 3432 sbcco2 3459 sbcie2g 3469 sbcralt 3510 sbcreu 3515 cbvralcsf 3565 cbvreucsf 3567 cbvrabcsf 3568 sbcel12 3983 sbceqg 3984 sbss 4084 sbcbr123 4706 cbvopab1 4723 cbvmpt 4749 wfis2fg 5717 cbviota 5856 cbvriota 6621 tfis2f 7055 tfinds 7059 nd1 9409 nd2 9410 rmo4fOLD 29336 rmo4f 29337 funcnv4mpt 29470 nn0min 29567 ballotlemodife 30559 bnj1321 31095 setinds2f 31684 frins2fg 31744 bj-clelsb3 32848 bj-sbeqALT 32895 prtlem5 34145 sbcrexgOLD 37349 sbcel12gOLD 38754 |
Copyright terms: Public domain | W3C validator |