![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfxfrd | Structured version Visualization version Unicode version |
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
nfbii.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
nfxfrd.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfxfrd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfxfrd.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | nfbii.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | nfbii 1695 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | sylibr 216 |
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 1669 ax-4 1682 |
This theorem depends on definitions: df-bi 189 df-nf 1668 |
This theorem is referenced by: nfand 2008 nf3and 2009 nfbid 2016 nfexd 2035 dvelimhw 2060 nfexd2 2166 dvelimf 2168 nfeud2 2311 nfmod2 2312 nfeqd 2599 nfeld 2600 nfabd2 2611 nfned 2724 nfneld 2732 nfrald 2773 nfrexd 2849 nfreud 2963 nfrmod 2964 nfsbc1d 3285 nfsbcd 3288 nfbrd 4446 wl-nfnbi 31859 wl-sb8eut 31906 |
Copyright terms: Public domain | W3C validator |