Theorem nfxfr 1771

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

Hypotheses

Ref	Expression
nfbii.1	⊢ (𝜑 ↔ 𝜓)
nfxfr.2	⊢ Ⅎ𝑥𝜓

Assertion

Ref	Expression
nfxfr	⊢ Ⅎ𝑥𝜑

Proof of Theorem nfxfr

Step	Hyp	Ref	Expression
1		nfxfr.2	. 2 ⊢ Ⅎ𝑥𝜓
2		nfbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	nfbii 1770	. 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
4	1, 3	mpbir 220	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:   ↔ wb 195  Ⅎwnf 1699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701

This theorem is referenced by:  nfanOLD  1817  nfnan  1818  nf3an  1819  nfor  1822  nf3or  1823  nfa1  2015  nfnf1  2018  nfa2  2027  nfan1  2056  nfex  2140  nfnf  2144  nfnf1OLD  2145  nfs1f  2371  nfeu1  2468  nfmo1  2469  nfnfc1  2754  nfnfc  2760  nfnfcALT  2761  nfne  2882  nfnel  2890  nfra1  2925  nfre1  2988  nfreu1  3089  nfrmo1  3090  nfrmo  3094  nfss  3561  nfdisj  4565  nfdisj1  4566  nfpo  4964  nfso  4965  nffr  5012  nfse  5013  nfwe  5014  nfrel  5127  sb8iota  5775  nffun  5826  nffn  5901  nff  5954  nff1  6012  nffo  6027  nff1o  6048  nfiso  6472  tz7.49  7427  nfixp  7813  bnj919  30091  bnj1379  30155  bnj571  30230  bnj607  30240  bnj873  30248  bnj981  30274  bnj1039  30293  bnj1128  30312  bnj1388  30355  bnj1398  30356  bnj1417  30363  bnj1444  30365  bnj1445  30366  bnj1446  30367  bnj1449  30370  bnj1467  30376  bnj1489  30378  bnj1312  30380  bnj1518  30386  bnj1525  30391  bj-nfnfc  32047  wl-nfae1  32494  wl-ax11-lem4  32544  ptrecube  32579  nfdfat  39859