Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nffv | GIF version |
Description: Bound-variable hypothesis builder for function value. (Contributed by NM, 14-Nov-1995.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Ref | Expression |
---|---|
nffv.1 | ⊢ Ⅎ𝑥𝐹 |
nffv.2 | ⊢ Ⅎ𝑥𝐴 |
Ref | Expression |
---|---|
nffv | ⊢ Ⅎ𝑥(𝐹‘𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fv 5191 | . 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦) | |
2 | nffv.2 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | nffv.1 | . . . 4 ⊢ Ⅎ𝑥𝐹 | |
4 | nfcv 2306 | . . . 4 ⊢ Ⅎ𝑥𝑦 | |
5 | 2, 3, 4 | nfbr 4023 | . . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦 |
6 | 5 | nfiotaw 5152 | . 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦) |
7 | 1, 6 | nfcxfr 2303 | 1 ⊢ Ⅎ𝑥(𝐹‘𝐴) |
Colors of variables: wff set class |
Syntax hints: Ⅎwnfc 2293 class class class wbr 3977 ℩cio 5146 ‘cfv 5183 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-3an 969 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-rex 2448 df-v 2724 df-un 3116 df-sn 3577 df-pr 3578 df-op 3580 df-uni 3785 df-br 3978 df-iota 5148 df-fv 5191 |
This theorem is referenced by: nffvmpt1 5492 nffvd 5493 dffn5imf 5536 fvmptssdm 5565 fvmptf 5573 eqfnfv2f 5582 ralrnmpt 5622 rexrnmpt 5623 ffnfvf 5639 funiunfvdmf 5727 dff13f 5733 nfiso 5769 nfrecs 6267 nffrec 6356 cc2 7200 nfseq 10381 seq3f1olemstep 10427 seq3f1olemp 10428 nfsum1 11287 nfsum 11288 fsumrelem 11402 nfcprod1 11485 nfcprod 11486 ctiunctlemfo 12335 ctiunct 12336 cnmpt11 12850 cnmpt21 12858 |
Copyright terms: Public domain | W3C validator |