Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfxfr | 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 1449 | . 2 |
4 | 1, 3 | mpbir 145 | 1 |
Colors of variables: wff set class |
Syntax hints: 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: nfnf1 1523 nf3an 1545 nfnf 1556 nfdc 1637 nfs1f 1753 nfeu1 2008 nfmo1 2009 sb8eu 2010 nfeu 2016 nfnfc1 2282 nfnfc 2286 nfeq 2287 nfel 2288 nfne 2399 nfnel 2408 nfra1 2464 nfre1 2474 nfreu1 2600 nfrmo1 2601 nfss 3085 rabn0m 3385 nfdisjv 3913 nfdisj1 3914 nfpo 4218 nfso 4219 nfse 4258 nffrfor 4265 nffr 4266 nfwe 4272 nfrel 4619 sb8iota 5090 nffun 5141 nffn 5214 nff 5264 nff1 5321 nffo 5339 nff1o 5358 nfiso 5700 nfixpxy 6604 |
Copyright terms: Public domain | W3C validator |