Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbcie | Structured version Visualization version Unicode version |
Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 4-Sep-2004.) |
Ref | Expression |
---|---|
sbcie.1 | |
sbcie.2 |
Ref | Expression |
---|---|
sbcie |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcie.1 | . 2 | |
2 | sbcie.2 | . . 3 | |
3 | 2 | sbcieg 3468 | . 2 |
4 | 1, 3 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wceq 1483 wcel 1990 cvv 3200 wsbc 3435 |
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-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-v 3202 df-sbc 3436 |
This theorem is referenced by: tfinds2 7063 findcard2 8200 ac6sfi 8204 ac6num 9301 fpwwe 9468 nn1suc 11041 wrdind 13476 cjth 13843 fprodser 14679 prmind2 15398 joinlem 17011 meetlem 17025 mrcmndind 17366 isghm 17660 islmod 18867 islindf 20151 fgcl 21682 cfinfil 21697 csdfil 21698 supfil 21699 fin1aufil 21736 quotval 24047 dfconngr1 27048 isconngr 27049 isconngr1 27050 bnj62 30786 bnj610 30817 bnj976 30848 bnj106 30938 bnj125 30942 bnj154 30948 bnj155 30949 bnj526 30958 bnj540 30962 bnj591 30981 bnj609 30987 bnj893 30998 bnj1417 31109 soseq 31751 poimirlem27 33436 sdclem2 33538 fdc 33541 fdc1 33542 lshpkrlem3 34399 hdmap1fval 37086 hdmapfval 37119 rabren3dioph 37379 2nn0ind 37510 zindbi 37511 onfrALTlem5 38757 |
Copyright terms: Public domain | W3C validator |