![]() |
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 1697 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpbir 213 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 |
This theorem depends on definitions: df-bi 189 df-nf 1670 |
This theorem is referenced by: nfnf1 1983 nfnan 2014 nf3an 2015 nfor 2020 nf3or 2021 nfnf 2034 nfs1f 2214 nfeu1 2311 nfmo1 2312 nfnfc1 2597 nfnfc 2603 nfnfcALT 2604 nfne 2725 nfnel 2733 nfra1 2771 nfre1 2850 nfrexOLD 2853 nfreu1 2963 nfrmo1 2964 nfrmo 2968 nfss 3427 nfdisj 4388 nfdisj1 4389 nfpo 4763 nfso 4764 nffr 4811 nfse 4812 nfwe 4813 nfrel 4923 sb8iota 5556 nffun 5607 nffn 5677 nff 5729 nff1 5782 nffo 5797 nff1o 5817 nfiso 6220 tz7.49 7167 nfixp 7546 bnj919 29590 bnj1379 29654 bnj571 29729 bnj607 29739 bnj873 29747 bnj981 29773 bnj1039 29792 bnj1128 29811 bnj1388 29854 bnj1398 29855 bnj1417 29862 bnj1444 29864 bnj1445 29865 bnj1446 29866 bnj1449 29869 bnj1467 29875 bnj1489 29877 bnj1312 29879 bnj1518 29885 bnj1525 29890 bj-nfnfc 31474 wl-nfae1 31872 wl-ax11-lem4 31930 ptrecube 31952 nfdfat 38642 |
Copyright terms: Public domain | W3C validator |