| 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 5278 | . 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦) | |
| 2 | nffv.2 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
| 3 | nffv.1 | . . . 4 ⊢ Ⅎ𝑥𝐹 | |
| 4 | nfcv 2347 | . . . 4 ⊢ Ⅎ𝑥𝑦 | |
| 5 | 2, 3, 4 | nfbr 4089 | . . 3 ⊢ Ⅎ𝑥 𝐴𝐹𝑦 |
| 6 | 5 | nfiotaw 5235 | . 2 ⊢ Ⅎ𝑥(℩𝑦𝐴𝐹𝑦) |
| 7 | 1, 6 | nfcxfr 2344 | 1 ⊢ Ⅎ𝑥(𝐹‘𝐴) |
| Colors of variables: wff set class |
| Syntax hints: Ⅎwnfc 2334 class class class wbr 4043 ℩cio 5229 ‘cfv 5270 |
| 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-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-ext 2186 |
| This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1375 df-nf 1483 df-sb 1785 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-rex 2489 df-v 2773 df-un 3169 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-br 4044 df-iota 5231 df-fv 5278 |
| This theorem is referenced by: nffvmpt1 5586 nffvd 5587 dffn5imf 5633 fvmptssdm 5663 fvmptf 5671 eqfnfv2f 5680 ralrnmpt 5721 rexrnmpt 5722 ffnfvf 5738 funiunfvdmf 5832 dff13f 5838 nfiso 5874 nfrecs 6392 nffrec 6481 cc2 7378 nfseq 10600 seq3f1olemstep 10657 seq3f1olemp 10658 nfsum1 11609 nfsum 11610 fsumrelem 11724 nfcprod1 11807 nfcprod 11808 ctiunctlemfo 12752 ctiunct 12753 prdsbas3 13061 cnmpt11 14697 cnmpt21 14705 lgseisenlem2 15490 |
| Copyright terms: Public domain | W3C validator |