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

Theorem nfxfr 1855
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 1854 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3mpbir 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