Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbcieg | Structured version Visualization version Unicode version |
Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
sbcieg.1 |
Ref | Expression |
---|---|
sbcieg |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1843 | . 2 | |
2 | sbcieg.1 | . 2 | |
3 | 1, 2 | sbciegf 3467 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wceq 1483 wcel 1990 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: sbcie 3470 ralsng 4218 rexsng 4219 rabsnif 4258 ralrnmpt 6368 fpwwe2lem3 9455 nn1suc 11041 opfi1uzind 13283 mrcmndind 17366 fgcl 21682 cfinfil 21697 csdfil 21698 supfil 21699 fin1aufil 21736 ifeqeqx 29361 nn0min 29567 bnj1452 31120 cdlemk35s 36225 cdlemk39s 36227 cdlemk42 36229 2nn0ind 37510 zindbi 37511 trsbcVD 39113 onfrALTlem5VD 39121 |
Copyright terms: Public domain | W3C validator |