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 1449 | . 2 |
4 | 1, 3 | sylibr 133 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wnf 1436 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 |
This theorem depends on definitions: df-bi 116 df-nf 1437 |
This theorem is referenced by: nf3and 1548 nfbid 1567 nfsbxy 1915 nfsbxyt 1916 nfeud 2015 nfmod 2016 nfeqd 2296 nfeld 2297 nfabd 2300 nfned 2402 nfneld 2411 nfraldxy 2467 nfrexdxy 2468 nfraldya 2469 nfrexdya 2470 nfsbc1d 2925 nfsbcd 2928 nfbrd 3973 |
Copyright terms: Public domain | W3C validator |