Metamath Proof Explorer
Description: A utility lemma to transfer a boundvariable hypothesis builder into a
definition. (Contributed by Mario Carneiro, 11Aug2016)


Ref 
Expression 

Hypotheses 
nfbii.1 
⊢ ( 𝜑 ↔ 𝜓 ) 


nfxfr.2 
⊢ Ⅎ 𝑥 𝜓 

Assertion 
nfxfr 
⊢ Ⅎ 𝑥 𝜑 
Proof
Step 
Hyp 
Ref 
Expression 
1 

nfbii.1 
⊢ ( 𝜑 ↔ 𝜓 ) 
2 

nfxfr.2 
⊢ Ⅎ 𝑥 𝜓 
3 
1

nfbii 
⊢ ( Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 𝜓 ) 
4 
2 3

mpbir 
⊢ Ⅎ 𝑥 𝜑 