![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfcv | GIF version |
Description: If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfcv | ⊢ ℲxA |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1418 | . 2 ⊢ Ⅎx y ∈ A | |
2 | 1 | nfci 2165 | 1 ⊢ ℲxA |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1390 Ⅎwnfc 2162 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-gen 1335 ax-17 1416 |
This theorem depends on definitions: df-bi 110 df-nf 1347 df-nfc 2164 |
This theorem is referenced by: nfcvd 2176 nfel 2183 nfeq1 2184 nfel1 2185 nfeq2 2186 nfel2 2187 nfcvf 2196 r2al 2337 r2ex 2338 nfraldxy 2350 nfrexdxy 2351 nfra2xy 2358 r19.12 2416 ralcom 2467 rexcom 2468 nfreudxy 2477 raleq 2499 rexeq 2500 reueq1 2501 rmoeq1 2502 cbvral 2523 cbvrex 2524 rabeq 2545 cbvrabv 2550 vtoclg 2607 vtocl2g 2611 vtoclga 2613 vtocl2ga 2615 vtocl3ga 2617 spcimdv 2631 spcimedv 2633 spcgv 2634 spcegv 2635 rspct 2643 rspc 2644 rspce 2645 rspc2 2655 ceqsexg 2666 elabgt 2678 elabf 2680 elabg 2682 elab3g 2687 elrab 2692 mob 2717 nfsbc1v 2776 elrabsf 2795 sbcralt 2828 sbcrext 2829 sbcralg 2830 sbcrexg 2831 sbcreug 2832 cbvcsbv 2851 csbconstg 2858 nfcsb1v 2876 csbnestg 2894 cbvralcsf 2902 cbvrexcsf 2903 cbvreucsf 2904 cbvrabcsf 2905 cbvralv2 2906 cbvrexv2 2907 n0rf 3227 n0r 3228 eq0 3233 raaanlem 3320 nfpw 3363 cbviunv 3687 cbviinv 3688 ssiun2s 3692 iunab 3694 ssiinf 3697 ssiin 3698 iinab 3709 cbvdisjv 3747 nfdisjv 3748 cbvmptv 3843 triun 3858 csbexga 3876 repizf2 3906 moop2 3979 euotd 3982 opelopabf 4002 nfpo 4029 nfso 4030 pofun 4040 nfse 4063 eusvnf 4151 rabxfrd 4167 tfis 4249 tfisi 4253 opeliunxp 4338 nfrel 4368 opeliunxp2 4419 ralxpf 4425 rexxpf 4426 nfco 4444 nfcnv 4457 dfdmf 4471 dfrnf 4518 nfdm 4521 nfres 4557 nfiotadxy 4813 dffun6f 4858 dffun6 4859 dffun4f 4861 nffun 4867 funimaexglem 4925 nffv 5128 nffvmpt1 5129 dffn5imf 5171 funfvdm2f 5181 fvmptss2 5190 fvmpts 5193 fvmpt2 5197 fvmptssdm 5198 mptfvex 5199 fvmptdv 5202 eqfnfv2f 5212 ralrnmpt 5252 rexrnmpt 5253 f1ompt 5263 ffnfvf 5267 fmptco 5273 fmptcof 5274 fmptcos 5275 funiunfvdmf 5346 dff13f 5352 f1mpt 5353 fliftfuns 5381 nfiso 5389 nfriotadxy 5419 csbriotag 5423 riota2 5433 mpt2eq123 5506 cbvmpt2x 5524 cbvmpt2 5525 cbvmpt2v 5526 ovmpt2s 5566 ov2gf 5567 ovmpt2dxf 5568 ovmpt2dx 5569 ovmpt2dv 5575 ovmpt2dv2 5576 ovi3 5579 nfof 5659 nfofr 5660 offval2 5668 ofrfval2 5669 abrexex2g 5689 abrexex2 5693 dfopab2 5757 dfoprab3s 5758 mpt2mptsx 5765 dmmpt2ssx 5767 fmpt2x 5768 mpt2fvex 5771 fmpt2co 5779 dfmpt2 5786 mpt2xopoveq 5796 mpt2xopovel 5797 nftpos 5835 tposoprab 5836 nfrecs 5863 nffrec 5921 eqerlem 6073 qliftfuns 6126 dom2lem 6188 xpcomco 6236 fzrevral 8737 nfiseq 8898 elabf1 9255 elabf2 9256 elabg2 9259 bj-omssind 9394 bj-bdfindisg 9408 bj-nntrans 9411 bj-nnelirr 9413 bj-omtrans 9416 setindis 9427 bdsetindis 9429 bj-nn0sucALT 9438 bj-findis 9439 bj-findisg 9440 strcollnfALT 9446 |
Copyright terms: Public domain | W3C validator |