| 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 3047 | 1 ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑 |
| Colors of variables: wff set class |
| Syntax hints: Ⅎwnf 1506 [wsbc 3029 |
| 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 3030 |
| This theorem is referenced by: elrabsf 3068 cbvralcsf 3188 cbvrexcsf 3189 rabsnifsb 3735 euotd 4345 findes 4699 omsinds 4718 elfvmptrab1 5737 ralrnmpt 5785 rexrnmpt 5786 elovmporab 6217 elovmporab1w 6218 uchoice 6295 dfopab2 6347 dfoprab3s 6348 mpoxopoveq 6401 findcard2 7071 findcard2s 7072 ac6sfi 7080 opabfi 7123 dcfi 7171 indpi 7552 nn0ind-raph 9587 uzind4s 9814 indstr 9817 fzrevral 10330 exfzdc 10476 zsupcllemstep 10479 infssuzex 10483 uzsinds 10696 prmind2 12682 gropd 15888 grstructd2dom 15889 bj-bdfindes 16480 bj-findes 16512 |
| Copyright terms: Public domain | W3C validator |