Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sbcex | Unicode version |
Description: By our definition of proper substitution, it can only be true if the substituted expression is a set. (Contributed by Mario Carneiro, 13-Oct-2016.) |
Ref | Expression |
---|---|
sbcex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sbc 2952 | . 2 | |
2 | elex 2737 | . 2 | |
3 | 1, 2 | sylbi 120 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 2136 cab 2151 cvv 2726 wsbc 2951 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1435 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-ext 2147 |
This theorem depends on definitions: df-bi 116 df-sb 1751 df-clab 2152 df-cleq 2158 df-clel 2161 df-v 2728 df-sbc 2952 |
This theorem is referenced by: sbcco 2972 sbc5 2974 sbcan 2993 sbcor 2995 sbcn1 2998 sbcim1 2999 sbcbi1 3000 sbcal 3002 sbcex2 3004 sbcel1v 3013 sbcel21v 3015 sbcimdv 3016 sbcrext 3028 spesbc 3036 csbprc 3454 opelopabsb 4238 |
Copyright terms: Public domain | W3C validator |