![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfxfr | Structured version Visualization version 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 1928 | . 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) |
4 | 1, 3 | mpbir 221 | 1 ⊢ Ⅎ𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 Ⅎwnf 1856 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 |
This theorem depends on definitions: df-bi 197 df-ex 1853 df-nf 1858 |
This theorem is referenced by: nfanOLD 1981 nfnan 1982 nf3an 1983 nfor 1986 nf3or 1987 nfa1 2184 nfnf1 2187 nfa2 2196 nfan1 2222 nfan1OLDOLD 2223 nfs1v 2274 nfex 2318 nfnf 2322 nfnf1OLD 2323 nfs1f 2530 nfeu1 2628 nfmo1 2629 nfnfc1 2916 nfnfc 2923 nfnfcALT 2924 nfne 3043 nfnel 3053 nfra1 3090 nfre1 3153 nfreu1 3258 nfrmo1 3259 nfrmo 3263 nfss 3745 nfdisj 4766 nfdisj1 4767 nfpo 5175 nfso 5176 nffr 5223 nfse 5224 nfwe 5225 nfrel 5344 sb8iota 6001 nffun 6054 nffn 6127 nff 6181 nff1 6239 nffo 6255 nff1o 6276 nfiso 6715 tz7.49 7693 nfixp 8081 bnj919 31175 bnj1379 31239 bnj571 31314 bnj607 31324 bnj873 31332 bnj981 31358 bnj1039 31377 bnj1128 31396 bnj1388 31439 bnj1398 31440 bnj1417 31447 bnj1444 31449 bnj1445 31450 bnj1446 31451 bnj1449 31454 bnj1467 31460 bnj1489 31462 bnj1312 31464 bnj1518 31470 bnj1525 31475 wl-nfae1 33650 wl-ax11-lem4 33699 ptrecube 33742 nfdfat 41730 |
Copyright terms: Public domain | W3C validator |