Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfcvd | GIF 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 2258 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | a1i 9 | 1 ⊢ (𝜑 → Ⅎ𝑥𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Ⅎwnfc 2245 |
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 1410 ax-17 1491 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-nfc 2247 |
This theorem is referenced by: nfeld 2274 vtoclgft 2710 vtocld 2712 sbcralt 2957 sbcrext 2958 csbied 3016 csbie2t 3018 sbcco3g 3027 csbco3g 3028 dfnfc2 3724 eusvnfb 4345 eusv2i 4346 peano2 4479 iota2d 5083 iota2 5084 fmptcof 5555 riota5f 5722 riota5 5723 fmpoco 6081 nfixpxy 6579 nfnegd 7926 iseqf1olemjpcl 10236 iseqf1olemqpcl 10237 iseqf1olemfvp 10238 seq3f1olemqsum 10241 strcollnft 13109 |
Copyright terms: Public domain | W3C validator |