![]() |
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 2240 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | a1i 9 | 1 ⊢ (𝜑 → Ⅎ𝑥𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Ⅎwnfc 2227 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1393 ax-17 1474 |
This theorem depends on definitions: df-bi 116 df-nf 1405 df-nfc 2229 |
This theorem is referenced by: nfeld 2256 vtoclgft 2691 vtocld 2693 sbcralt 2937 sbcrext 2938 csbied 2996 csbie2t 2998 sbcco3g 3007 csbco3g 3008 dfnfc2 3701 eusvnfb 4313 eusv2i 4314 peano2 4447 iota2d 5049 iota2 5050 fmptcof 5519 riota5f 5686 riota5 5687 fmpoco 6043 nfixpxy 6541 nfnegd 7829 iseqf1olemjpcl 10109 iseqf1olemqpcl 10110 iseqf1olemfvp 10111 seq3f1olemqsum 10114 strcollnft 12767 |
Copyright terms: Public domain | W3C validator |