MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfxfr Structured version   Visualization version   GIF version

Theorem nfxfr 1854
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nfbii.1 (𝜑𝜓)
nfxfr.2 𝑥𝜓
Assertion
Ref Expression
nfxfr 𝑥𝜑

Proof of Theorem nfxfr
StepHypRef Expression
1 nfxfr.2 . 2 𝑥𝜓
2 nfbii.1 . . 3 (𝜑𝜓)
32nfbii 1853 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3mpbir 234 1 𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 209  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 210  df-ex 1782  df-nf 1786
This theorem is referenced by:  nfnan  1901  nf3an  1902  nfor  1905  nf3or  1906  nfa1  2153  nfnf1  2156  nfs1v  2158  nfa2  2175  nfan1  2199  nfs1f  2274  nfex  2335  nfnf  2337  nfsbv  2341  nfsbvOLD  2342  nfmo1  2619  nfeu1  2652  nfeu1ALT  2653  nfsab1  2788  nfnfc1  2961  nfnfc  2970  nfabdw  2979  nfne  3090  nfnel  3101  nfra1  3186  nfre1  3268  r19.12  3286  nfreu1  3326  nfrmo1  3327  nfrmow  3331  nfrmo  3333  nfss  3910  nfdisjw  5010  nfdisj  5011  nfdisj1  5012  nfpo  5447  nfso  5448  nffr  5497  nfse  5498  nfwe  5499  nfrel  5622  sb8iota  6298  nffun  6351  nffn  6426  nff  6487  nff1  6551  nffo  6568  nff1o  6592  nfiso  7058  tz7.49  8068  nfixpw  8467  nfixp  8468  bnj919  32152  bnj1379  32216  bnj571  32292  bnj607  32302  bnj873  32310  bnj981  32336  bnj1039  32357  bnj1128  32376  bnj1388  32419  bnj1398  32420  bnj1417  32427  bnj1444  32429  bnj1445  32430  bnj1446  32431  bnj1449  32434  bnj1467  32440  bnj1489  32442  bnj1312  32444  bnj1518  32450  bnj1525  32455  wl-nfae1  34931  wl-ax11-lem4  34984  ptrecube  35056  nfdfat  43680  nfich1  43961  nfich2  43962  ichnfimlem  43977  ich2ex  43982
  Copyright terms: Public domain W3C validator