Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfrn | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Ref | Expression |
---|---|
nfrn.1 | ⊢ Ⅎ𝑥𝐴 |
Ref | Expression |
---|---|
nfrn | ⊢ Ⅎ𝑥ran 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rn 5049 | . 2 ⊢ ran 𝐴 = dom ◡𝐴 | |
2 | nfrn.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcnv 5223 | . . 3 ⊢ Ⅎ𝑥◡𝐴 |
4 | 3 | nfdm 5288 | . 2 ⊢ Ⅎ𝑥dom ◡𝐴 |
5 | 1, 4 | nfcxfr 2749 | 1 ⊢ Ⅎ𝑥ran 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnfc 2738 ◡ccnv 5037 dom cdm 5038 ran crn 5039 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644 df-cnv 5046 df-dm 5048 df-rn 5049 |
This theorem is referenced by: nfima 5393 nff 5954 nffo 6027 fliftfun 6462 zfrep6 7027 ptbasfi 21194 utopsnneiplem 21861 restmetu 22185 itg2cnlem1 23334 acunirnmpt2 28842 acunirnmpt2f 28843 locfinreflem 29235 esumrnmpt2 29457 esumgect 29479 esum2d 29482 esumiun 29483 sigapildsys 29552 ldgenpisyslem1 29553 oms0 29686 bnj1366 30154 totbndbnd 32758 refsumcn 38212 suprnmpt 38350 wessf1ornlem 38366 disjrnmpt2 38370 disjf1o 38373 disjinfi 38375 choicefi 38387 stoweidlem27 38920 stoweidlem29 38922 stoweidlem31 38924 stoweidlem35 38928 stoweidlem59 38952 stoweidlem62 38955 stirlinglem5 38971 fourierdlem31 39031 fourierdlem53 39052 fourierdlem80 39079 fourierdlem93 39092 sge00 39269 sge0f1o 39275 sge0gerp 39288 sge0pnffigt 39289 sge0lefi 39291 sge0ltfirp 39293 sge0resplit 39299 sge0reuz 39340 iunhoiioolem 39566 |
Copyright terms: Public domain | W3C validator |