Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfxfr | Structured version Visualization version Unicode version |
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfbii.1 | |
nfxfr.2 |
Ref | Expression |
---|---|
nfxfr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfxfr.2 | . 2 | |
2 | nfbii.1 | . . 3 | |
3 | 2 | nfbii 1778 | . 2 |
4 | 1, 3 | mpbir 221 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wnf 1708 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-ex 1705 df-nf 1710 |
This theorem is referenced by: nfanOLD 1829 nfnan 1830 nf3an 1831 nfor 1834 nf3or 1835 nfa1 2028 nfnf1 2031 nfa2 2040 nfan1 2068 nfex 2154 nfnf 2158 nfnf1OLD 2159 nfs1f 2383 nfeu1 2480 nfmo1 2481 nfnfc1 2767 nfnfc 2774 nfnfcALT 2775 nfne 2894 nfnel 2904 nfra1 2941 nfre1 3005 nfreu1 3110 nfrmo1 3111 nfrmo 3115 nfss 3596 nfdisj 4632 nfdisj1 4633 nfpo 5040 nfso 5041 nffr 5088 nfse 5089 nfwe 5090 nfrel 5204 sb8iota 5858 nffun 5911 nffn 5987 nff 6041 nff1 6099 nffo 6114 nff1o 6135 nfiso 6572 tz7.49 7540 nfixp 7927 bnj919 30837 bnj1379 30901 bnj571 30976 bnj607 30986 bnj873 30994 bnj981 31020 bnj1039 31039 bnj1128 31058 bnj1388 31101 bnj1398 31102 bnj1417 31109 bnj1444 31111 bnj1445 31112 bnj1446 31113 bnj1449 31116 bnj1467 31122 bnj1489 31124 bnj1312 31126 bnj1518 31132 bnj1525 31137 bj-nfnfc 32853 wl-nfae1 33315 wl-ax11-lem4 33365 ptrecube 33409 nfdfat 41210 |
Copyright terms: Public domain | W3C validator |