Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfxfr | GIF 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 1402 | . 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) |
4 | 1, 3 | mpbir 144 | 1 ⊢ Ⅎ𝑥𝜑 |
Colors of variables: wff set class |
Syntax hints: ↔ wb 103 Ⅎwnf 1389 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-gen 1378 |
This theorem depends on definitions: df-bi 115 df-nf 1390 |
This theorem is referenced by: nfnf1 1476 nf3an 1498 nfnf 1509 nfdc 1589 nfs1f 1703 nfeu1 1952 nfmo1 1953 sb8eu 1954 nfeu 1960 nfnfc1 2222 nfnfc 2225 nfeq 2226 nfel 2227 nfne 2337 nfnel 2346 nfra1 2397 nfre1 2407 nfreu1 2525 nfrmo1 2526 nfss 2992 rabn0m 3272 nfdisjv 3778 nfdisj1 3779 nfpo 4056 nfso 4057 nfse 4096 nffrfor 4103 nffr 4104 nfwe 4110 nfrel 4443 sb8iota 4894 nffun 4944 nffn 5015 nff 5063 nff1 5110 nffo 5125 nff1o 5144 nfiso 5466 |
Copyright terms: Public domain | W3C validator |