Metamath Proof Explorer


Theorem nfcxfrd

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

Ref Expression
Hypotheses nfcxfr.1
|- A = B
nfcxfrd.2
|- ( ph -> F/_ x B )
Assertion nfcxfrd
|- ( ph -> F/_ x A )

Proof

Step Hyp Ref Expression
1 nfcxfr.1
 |-  A = B
2 nfcxfrd.2
 |-  ( ph -> F/_ x B )
3 1 nfceqi
 |-  ( F/_ x A <-> F/_ x B )
4 2 3 sylibr
 |-  ( ph -> F/_ x A )