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 1843 | . 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) |
4 | 1, 3 | mpbir 232 | 1 ⊢ Ⅎ𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 Ⅎwnf 1775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-ex 1772 df-nf 1776 |
This theorem is referenced by: nfnan 1892 nf3an 1893 nfor 1896 nf3or 1897 nfa1 2146 nfnf1 2149 nfa2 2166 nfan1 2190 nfs1v 2264 nfs1f 2266 nfex 2334 nfnf 2336 nfsbv 2340 nfsbvOLD 2341 nfmo1 2634 nfeu1 2667 nfeu1ALT 2668 nfsab1 2805 nfnfc1 2977 nfnfc 2987 nfabdw 2997 nfne 3116 nfnel 3127 nfra1 3216 nfre1 3303 r19.12 3321 nfreu1 3368 nfrmo1 3369 nfrmow 3373 nfrmo 3375 nfss 3957 nfdisjw 5034 nfdisj 5035 nfdisj1 5036 nfpo 5472 nfso 5473 nffr 5522 nfse 5523 nfwe 5524 nfrel 5647 sb8iota 6318 nffun 6371 nffn 6445 nff 6503 nff1 6566 nffo 6582 nff1o 6606 nfiso 7064 tz7.49 8070 nfixpw 8468 nfixp 8469 bnj919 31937 bnj1379 32001 bnj571 32077 bnj607 32087 bnj873 32095 bnj981 32121 bnj1039 32140 bnj1128 32159 bnj1388 32202 bnj1398 32203 bnj1417 32210 bnj1444 32212 bnj1445 32213 bnj1446 32214 bnj1449 32217 bnj1467 32223 bnj1489 32225 bnj1312 32227 bnj1518 32233 bnj1525 32238 wl-nfae1 34649 wl-ax11-lem4 34701 ptrecube 34773 nfdfat 43203 nfich1 43484 nfich2 43485 ich2ex 43506 |
Copyright terms: Public domain | W3C validator |