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

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