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


Ref 
Expression 

Hypotheses 
nfbii.1 
⊢ ( 𝜑 ↔ 𝜓 ) 


nfxfrd.2 
⊢ ( 𝜒 → Ⅎ 𝑥 𝜓 ) 

Assertion 
nfxfrd 
⊢ ( 𝜒 → Ⅎ 𝑥 𝜑 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

nfbii.1 
⊢ ( 𝜑 ↔ 𝜓 ) 
2 

nfxfrd.2 
⊢ ( 𝜒 → Ⅎ 𝑥 𝜓 ) 
3 
1

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

sylibr 
⊢ ( 𝜒 → Ⅎ 𝑥 𝜑 ) 