Metamath Proof Explorer


Theorem nfxfr

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Hypotheses nfbii.1
|- ( ph <-> ps )
nfxfr.2
|- F/ x ps
Assertion nfxfr
|- F/ x ph

Proof

Step Hyp Ref Expression
1 nfbii.1
 |-  ( ph <-> ps )
2 nfxfr.2
 |-  F/ x ps
3 1 nfbii
 |-  ( F/ x ph <-> F/ x ps )
4 2 3 mpbir
 |-  F/ x ph