| 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 2372 | . 2 ⊢ Ⅎ𝑥𝐴 | |
| 2 | 1 | nfsbc1 3046 | 1 ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑 |
| Colors of variables: wff set class |
| Syntax hints: Ⅎwnf 1506 [wsbc 3028 |
| 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 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-11 1552 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-ext 2211 |
| This theorem depends on definitions: df-bi 117 df-tru 1398 df-nf 1507 df-sb 1809 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-sbc 3029 |
| This theorem is referenced by: elrabsf 3067 cbvralcsf 3187 cbvrexcsf 3188 euotd 4341 findes 4695 omsinds 4714 elfvmptrab1 5729 ralrnmpt 5777 rexrnmpt 5778 elovmporab 6205 elovmporab1w 6206 uchoice 6283 dfopab2 6335 dfoprab3s 6336 mpoxopoveq 6386 findcard2 7051 findcard2s 7052 ac6sfi 7060 opabfi 7100 dcfi 7148 indpi 7529 nn0ind-raph 9564 uzind4s 9785 indstr 9788 fzrevral 10301 exfzdc 10446 zsupcllemstep 10449 infssuzex 10453 uzsinds 10666 prmind2 12642 gropd 15848 grstructd2dom 15849 bj-bdfindes 16312 bj-findes 16344 |
| Copyright terms: Public domain | W3C validator |