![]() |
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 1834 | . 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) |
4 | 1, 3 | mpbir 232 | 1 ⊢ Ⅎ𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 Ⅎwnf 1766 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 |
This theorem depends on definitions: df-bi 208 df-ex 1763 df-nf 1767 |
This theorem is referenced by: nfnan 1883 nf3an 1884 nfor 1887 nf3or 1888 nfa1 2120 nfnf1 2123 nfa2 2139 nfan1 2164 nfs1v 2236 nfs1f 2238 nfex 2305 nfnf 2307 nfsbv 2311 nfsbvOLD 2312 2sb8evOLD 2331 nfmo1 2596 nfeu1 2634 nfeu1ALT 2635 nfsab1 2783 nfnfc1 2951 nfnfc 2958 nfne 3086 nfnel 3096 nfra1 3185 nfre1 3268 r19.12 3284 nfreu1 3330 nfrmo1 3331 nfrmo 3335 nfss 3884 nfdisj 4944 nfdisj1 4945 nfpo 5370 nfso 5371 nffr 5420 nfse 5421 nfwe 5422 nfrel 5543 sb8iota 6199 nffun 6251 nffn 6325 nff 6381 nff1 6444 nffo 6460 nff1o 6484 nfiso 6941 tz7.49 7935 nfixp 8332 bnj919 31647 bnj1379 31711 bnj571 31786 bnj607 31796 bnj873 31804 bnj981 31830 bnj1039 31849 bnj1128 31868 bnj1388 31911 bnj1398 31912 bnj1417 31919 bnj1444 31921 bnj1445 31922 bnj1446 31923 bnj1449 31926 bnj1467 31932 bnj1489 31934 bnj1312 31936 bnj1518 31942 bnj1525 31947 wl-nfae1 34313 wl-ax11-lem4 34364 ptrecube 34436 nfdfat 42856 nfich1 43103 nfich2 43104 ich2ex 43125 |
Copyright terms: Public domain | W3C validator |