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 2312 | . 2 | |
2 | 1 | a1i 9 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wnfc 2299 |
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-gen 1442 ax-17 1519 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-nfc 2301 |
This theorem is referenced by: nfeld 2328 nfraldw 2502 vtoclgft 2780 vtocld 2782 sbcralt 3031 sbcrext 3032 csbied 3095 csbie2t 3097 sbcco3g 3106 csbco3g 3107 dfnfc2 3814 eusvnfb 4439 eusv2i 4440 peano2 4579 iota2d 5185 iota2 5188 fmptcof 5663 riota5f 5833 riota5 5834 fmpoco 6195 nfixpxy 6695 nfnegd 8115 iseqf1olemjpcl 10451 iseqf1olemqpcl 10452 iseqf1olemfvp 10453 seq3f1olemqsum 10456 fprodeq0g 11601 pcmpt 12295 strcollnft 14019 |
Copyright terms: Public domain | W3C validator |