| 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 1852 | . 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) |
| 4 | 1, 3 | mpbir 231 | 1 ⊢ Ⅎ𝑥𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 Ⅎwnf 1783 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: nfnan 1900 nf3an 1901 nfor 1904 nf3or 1905 nfa1 2151 nfnf1 2154 nfs1v 2156 nfa2 2176 nfan1 2200 nfs1f 2275 nfex 2324 nfnf 2326 nfsbvOLD 2331 nfmo1 2557 nfeu1 2588 nfeu1ALT 2589 nfsab1 2722 nfnfc1 2908 nfaba1 2913 nfnfc 2918 nfne 3043 nfnel 3054 nfra1 3284 nfre1 3285 nfra2w 3299 nfra2wOLD 3300 r19.12 3314 r19.12OLD 3315 nfrmo1 3411 nfreu1 3412 nfrmow 3413 nfreuw 3414 nfrmowOLD 3427 nfrmo 3434 nfss 3976 nfdif 4129 nfun 4170 nfin 4224 nfiu1 5027 nfdisjw 5122 nfdisj 5123 nfdisj1 5124 nfpo 5598 nfso 5599 nffr 5658 nfse 5659 nfwe 5660 nfrel 5789 sb8iota 6525 nffun 6589 nffn 6667 nff 6732 nff1 6802 nffo 6819 nff1o 6846 nfiso 7342 tz7.49 8485 nfixpw 8956 nfixp 8957 bnj919 34781 bnj1379 34844 bnj571 34920 bnj607 34930 bnj873 34938 bnj981 34964 bnj1039 34985 bnj1128 35004 bnj1388 35047 bnj1398 35048 bnj1417 35055 bnj1444 35057 bnj1445 35058 bnj1446 35059 bnj1449 35062 bnj1467 35068 bnj1489 35070 bnj1312 35072 bnj1518 35078 bnj1525 35083 wl-nfae1 37528 wl-ax11-lem4 37589 ptrecube 37627 nfa1w 42685 nfrelp 44970 nfdfat 47139 nfich1 47434 nfich2 47435 ichnfimlem 47450 ich2ex 47455 |
| Copyright terms: Public domain | W3C validator |