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

Theorem nfxfrd 1646
 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 1644 . 2
41, 3sylibr 212 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  F/wnf 1616 This theorem is referenced by:  nfand  1925  nf3and  1926  nfbid  1933  nfexd  1952  dvelimhw  1955  nfexd2  2074  dvelimf  2076  nfeud2  2296  nfmod2  2297  nfeqd  2626  nfeld  2627  nfabd2  2640  nfned  2789  nfneld  2801  nfrald  2842  nfrexd  2919  nfreud  3030  nfrmod  3031  nfsbc1d  3345  nfsbcd  3348  nfbrd  4495  wl-nfnbi  29979  wl-sb8eut  30022 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631 This theorem depends on definitions:  df-bi 185  df-nf 1617
 Copyright terms: Public domain W3C validator