![]() |
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 2329 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | a1i 9 | 1 ⊢ (𝜑 → Ⅎ𝑥𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Ⅎwnfc 2316 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-gen 1459 ax-17 1536 |
This theorem depends on definitions: df-bi 117 df-nf 1471 df-nfc 2318 |
This theorem is referenced by: nfeld 2345 nfraldw 2519 vtoclgft 2799 vtocld 2801 sbcralt 3051 sbcrext 3052 csbied 3115 csbie2t 3117 sbcco3g 3126 csbco3g 3127 dfnfc2 3839 eusvnfb 4466 eusv2i 4467 peano2 4606 iota2d 5215 iota2 5218 fmptcof 5696 riota5f 5868 riota5 5869 fmpoco 6231 nfixpxy 6731 nfnegd 8167 iseqf1olemjpcl 10509 iseqf1olemqpcl 10510 iseqf1olemfvp 10511 seq3f1olemqsum 10514 fprodeq0g 11660 pcmpt 12355 strcollnft 15032 |
Copyright terms: Public domain | W3C validator |