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 3812 eusvnfb 4437 eusv2i 4438 peano2 4577 iota2d 5183 iota2 5186 fmptcof 5661 riota5f 5831 riota5 5832 fmpoco 6193 nfixpxy 6693 nfnegd 8108 iseqf1olemjpcl 10444 iseqf1olemqpcl 10445 iseqf1olemfvp 10446 seq3f1olemqsum 10449 fprodeq0g 11594 pcmpt 12288 strcollnft 13984 |
Copyright terms: Public domain | W3C validator |