Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfcvd | Unicode version |
Description: If is disjoint from , then is not free in . (Contributed by Mario Carneiro, 7-Oct-2016.) |
Ref | Expression |
---|---|
nfcvd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2178 | . 2 | |
2 | 1 | a1i 9 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wnfc 2165 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-gen 1338 ax-17 1419 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-nfc 2167 |
This theorem is referenced by: nfeld 2193 vtoclgft 2604 vtocld 2606 sbcralt 2834 sbcrext 2835 csbied 2892 csbie2t 2894 sbcco3g 2903 csbco3g 2904 dfnfc2 3598 eusvnfb 4186 eusv2i 4187 peano2 4318 iota2d 4892 iota2 4893 fmptcof 5331 riota5f 5492 riota5 5493 fmpt2co 5837 nfnegd 7207 strcollnft 10109 |
Copyright terms: Public domain | W3C validator |