![]() |
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 4251 findes 4599 omsinds 4618 elfvmptrab1 5606 ralrnmpt 5654 rexrnmpt 5655 dfopab2 6184 dfoprab3s 6185 mpoxopoveq 6235 findcard2 6883 findcard2s 6884 ac6sfi 6892 dcfi 6974 indpi 7332 nn0ind-raph 9359 uzind4s 9579 indstr 9582 fzrevral 10091 exfzdc 10226 uzsinds 10428 zsupcllemstep 11929 infssuzex 11933 prmind2 12103 bj-bdfindes 14357 bj-findes 14389 |
Copyright terms: Public domain | W3C validator |