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

Theorem nfxfr 1819
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 1818 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3mpbir 221 1 𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 196  wnf 1748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750
This theorem is referenced by:  nfanOLD  1869  nfnan  1870  nf3an  1871  nfor  1874  nf3or  1875  nfa1  2068  nfnf1  2071  nfa2  2080  nfan1  2106  nfex  2192  nfnf  2196  nfnf1OLD  2197  nfs1f  2411  nfeu1  2508  nfmo1  2509  nfnfc1  2796  nfnfc  2803  nfnfcALT  2804  nfne  2923  nfnel  2933  nfra1  2970  nfre1  3034  nfreu1  3139  nfrmo1  3140  nfrmo  3144  nfss  3629  nfdisj  4664  nfdisj1  4665  nfpo  5069  nfso  5070  nffr  5117  nfse  5118  nfwe  5119  nfrel  5238  sb8iota  5896  nffun  5949  nffn  6025  nff  6079  nff1  6137  nffo  6152  nff1o  6173  nfiso  6612  tz7.49  7585  nfixp  7969  bnj919  30963  bnj1379  31027  bnj571  31102  bnj607  31112  bnj873  31120  bnj981  31146  bnj1039  31165  bnj1128  31184  bnj1388  31227  bnj1398  31228  bnj1417  31235  bnj1444  31237  bnj1445  31238  bnj1446  31239  bnj1449  31242  bnj1467  31248  bnj1489  31250  bnj1312  31252  bnj1518  31258  bnj1525  31263  bj-nfnfc  32978  wl-nfae1  33445  wl-ax11-lem4  33495  ptrecube  33539  nfdfat  41531
  Copyright terms: Public domain W3C validator