![]() |
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 1854 | . 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) |
4 | 1, 3 | mpbir 230 | 1 ⊢ Ⅎ𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 Ⅎwnf 1785 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 |
This theorem depends on definitions: df-bi 206 df-ex 1782 df-nf 1786 |
This theorem is referenced by: nfnan 1903 nf3an 1904 nfor 1907 nf3or 1908 nfa1 2148 nfnf1 2151 nfs1v 2153 nfa2 2170 nfan1 2193 nfs1f 2266 nfex 2317 nfnf 2319 nfsbvOLD 2324 nfmo1 2555 nfeu1 2586 nfeu1ALT 2587 nfsab1 2721 nfnfc1 2909 nfnfc 2918 nfabdwOLD 2930 nfne 3044 nfnel 3055 nfra1 3266 nfre1 3267 nfra2w 3281 nfra2wOLD 3282 r19.12 3296 r19.12OLD 3297 nfrmo1 3383 nfreu1 3384 nfrmow 3385 nfreuw 3386 nfrmowOLD 3397 nfrmo 3404 nfss 3935 nfdisjw 5081 nfdisj 5082 nfdisj1 5083 nfpo 5549 nfso 5550 nffr 5606 nfse 5607 nfwe 5608 nfrel 5734 sb8iota 6458 nffun 6522 nffn 6599 nff 6662 nff1 6734 nffo 6753 nff1o 6780 nfiso 7264 tz7.49 8388 nfixpw 8851 nfixp 8852 bnj919 33270 bnj1379 33333 bnj571 33409 bnj607 33419 bnj873 33427 bnj981 33453 bnj1039 33474 bnj1128 33493 bnj1388 33536 bnj1398 33537 bnj1417 33544 bnj1444 33546 bnj1445 33547 bnj1446 33548 bnj1449 33551 bnj1467 33557 bnj1489 33559 bnj1312 33561 bnj1518 33567 bnj1525 33572 wl-nfae1 35975 wl-ax11-lem4 36029 ptrecube 36067 nfdfat 45329 nfich1 45609 nfich2 45610 ichnfimlem 45625 ich2ex 45630 |
Copyright terms: Public domain | W3C validator |