![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfcsb1v | GIF version |
Description: Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.) |
Ref | Expression |
---|---|
nfcsb1v | ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2235 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | nfcsb1 2976 | 1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵 |
Colors of variables: wff set class |
Syntax hints: Ⅎwnfc 2222 ⦋csb 2947 |
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-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-sbc 2855 df-csb 2948 |
This theorem is referenced by: csbhypf 2980 csbiebt 2981 sbcnestgf 2993 csbnest1g 2997 cbvralcsf 3004 cbvrexcsf 3005 cbvreucsf 3006 cbvrabcsf 3007 csbing 3222 disjnims 3859 disjiun 3862 sbcbrg 3916 moop2 4102 pofun 4163 eusvnf 4303 opeliunxp 4522 elrnmpt1 4718 resmptf 4795 csbima12g 4826 fvmpts 5417 fvmpt2 5422 mptfvex 5424 fmptco 5503 fmptcof 5504 fmptcos 5505 elabrex 5575 fliftfuns 5615 csbov123g 5725 ovmpt2s 5806 mpt2mptsx 6005 dmmpt2ssx 6007 fmpt2x 6008 mpt2fvex 6011 fmpt2co 6019 dfmpt2 6026 f1od2 6038 disjxp1 6039 eqerlem 6363 qliftfuns 6416 mptelixpg 6531 xpf1o 6640 iunfidisj 6735 seq3f1olemstep 10067 seq3f1olemp 10068 nfsum1 10915 sumeq2 10918 sumfct 10933 sumrbdclem 10935 summodclem3 10939 summodclem2a 10940 zsumdc 10943 fsumgcl 10945 fsum3 10946 isumss 10950 isumss2 10952 fsum3cvg2 10953 fsumzcl2 10964 fsumsplitf 10967 sumsnf 10968 sumsns 10974 fsumsplitsnun 10978 fsum2dlemstep 10993 fisumcom2 10997 fsumshftm 11004 fisum0diag2 11006 fsummulc2 11007 fsum00 11021 fsumabs 11024 fsumrelem 11030 fsumiun 11036 isumshft 11049 mertenslem2 11095 iuncld 11983 |
Copyright terms: Public domain | W3C validator |