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 1460 | . 2 |
4 | 1, 3 | mpbir 145 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wnf 1447 |
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 1434 ax-gen 1436 |
This theorem depends on definitions: df-bi 116 df-nf 1448 |
This theorem is referenced by: nfnf1 1531 nf3an 1553 nfnf 1564 nfdc 1646 nfs1f 1767 nfsbv 1934 nfeu1 2024 nfmo1 2025 sb8eu 2026 nfeu 2032 nfnfc1 2309 nfnfc 2313 nfeq 2314 nfel 2315 nfabdw 2325 nfne 2427 nfnel 2436 nfra1 2495 nfre1 2507 nfreu1 2635 nfrmo1 2636 nfss 3130 rabn0m 3431 nfdisjv 3965 nfdisj1 3966 nfpo 4273 nfso 4274 nfse 4313 nffrfor 4320 nffr 4321 nfwe 4327 nfrel 4683 sb8iota 5154 nffun 5205 nffn 5278 nff 5328 nff1 5385 nffo 5403 nff1o 5424 nfiso 5768 nfixpxy 6674 |
Copyright terms: Public domain | W3C validator |