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

Theorem nfxfr 1776
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 1775 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3mpbir 221 1 𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 196  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-ex 1702  df-nf 1707
This theorem is referenced by:  nfanOLD  1826  nfnan  1827  nf3an  1828  nfor  1831  nf3or  1832  nfa1  2025  nfnf1  2028  nfa2  2037  nfan1  2066  nfex  2151  nfnf  2155  nfnf1OLD  2156  nfs1f  2382  nfeu1  2479  nfmo1  2480  nfnfc1  2764  nfnfc  2770  nfnfcALT  2771  nfne  2890  nfnel  2900  nfra1  2936  nfre1  2999  nfreu1  3100  nfrmo1  3101  nfrmo  3105  nfss  3576  nfdisj  4595  nfdisj1  4596  nfpo  5000  nfso  5001  nffr  5048  nfse  5049  nfwe  5050  nfrel  5165  sb8iota  5817  nffun  5870  nffn  5945  nff  5998  nff1  6056  nffo  6071  nff1o  6092  nfiso  6526  tz7.49  7485  nfixp  7871  bnj919  30545  bnj1379  30609  bnj571  30684  bnj607  30694  bnj873  30702  bnj981  30728  bnj1039  30747  bnj1128  30766  bnj1388  30809  bnj1398  30810  bnj1417  30817  bnj1444  30819  bnj1445  30820  bnj1446  30821  bnj1449  30824  bnj1467  30830  bnj1489  30832  bnj1312  30834  bnj1518  30840  bnj1525  30845  bj-nfnfc  32500  wl-nfae1  32947  wl-ax11-lem4  32997  ptrecube  33041  nfdfat  40514
  Copyright terms: Public domain W3C validator