![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfxfrd | 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 1359 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | sylibr 137 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 |
This theorem depends on definitions: df-bi 110 df-nf 1347 |
This theorem is referenced by: nf3and 1458 nfbid 1477 nfsbxy 1815 nfsbxyt 1816 nfeud 1913 nfmod 1914 nfeqd 2189 nfeld 2190 nfabd 2193 nfned 2292 nfneld 2299 nfraldxy 2350 nfrexdxy 2351 nfraldya 2352 nfrexdya 2353 nfsbc1d 2774 nfsbcd 2777 nfbrd 3798 |
Copyright terms: Public domain | W3C validator |