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

Theorem nfxfrd 1697
 Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
nfbii.1
nfxfrd.2
Assertion
Ref Expression
nfxfrd

Proof of Theorem nfxfrd
StepHypRef Expression
1 nfxfrd.2 . 2
2 nfbii.1 . . 3
32nfbii 1695 . 2
41, 3sylibr 216 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188  wnf 1667 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682 This theorem depends on definitions:  df-bi 189  df-nf 1668 This theorem is referenced by:  nfand  2008  nf3and  2009  nfbid  2016  nfexd  2035  dvelimhw  2060  nfexd2  2166  dvelimf  2168  nfeud2  2311  nfmod2  2312  nfeqd  2599  nfeld  2600  nfabd2  2611  nfned  2724  nfneld  2732  nfrald  2773  nfrexd  2849  nfreud  2963  nfrmod  2964  nfsbc1d  3285  nfsbcd  3288  nfbrd  4446  wl-nfnbi  31859  wl-sb8eut  31906
 Copyright terms: Public domain W3C validator