![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfsbc1v | GIF version |
Description: Bound-variable hypothesis builder for class substitution. (Contributed by Mario Carneiro, 12-Oct-2016.) |
Ref | Expression |
---|---|
nfsbc1v | ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2319 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | nfsbc1 2980 | 1 ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑 |
Colors of variables: wff set class |
Syntax hints: Ⅎwnf 1460 [wsbc 2962 |
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-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-sbc 2963 |
This theorem is referenced by: elrabsf 3001 cbvralcsf 3119 cbvrexcsf 3120 euotd 4252 findes 4600 omsinds 4619 elfvmptrab1 5607 ralrnmpt 5655 rexrnmpt 5656 dfopab2 6185 dfoprab3s 6186 mpoxopoveq 6236 findcard2 6884 findcard2s 6885 ac6sfi 6893 dcfi 6975 indpi 7336 nn0ind-raph 9364 uzind4s 9584 indstr 9587 fzrevral 10098 exfzdc 10233 uzsinds 10435 zsupcllemstep 11936 infssuzex 11940 prmind2 12110 bj-bdfindes 14472 bj-findes 14504 |
Copyright terms: Public domain | W3C validator |