Theorem nfxfr 1856

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 1855	. 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
4	1, 3	mpbir 230	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:   ↔ wb 205  Ⅎwnf 1786

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

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfnan  1904  nf3an  1905  nfor  1908  nf3or  1909  nfa1  2149  nfnf1  2152  nfs1v  2154  nfa2  2171  nfan1  2194  nfs1f  2267  nfex  2318  nfnf  2320  nfsbvOLD  2325  nfmo1  2552  nfeu1  2583  nfeu1ALT  2584  nfsab1  2718  nfnfc1  2907  nfnfc  2916  nfabdwOLD  2928  nfne  3044  nfnel  3055  nfra1  3282  nfre1  3283  nfra2w  3297  nfra2wOLD  3298  r19.12  3312  r19.12OLD  3313  nfrmo1  3408  nfreu1  3409  nfrmow  3410  nfreuw  3411  nfrmowOLD  3424  nfrmo  3431  nfss  3975  nfdisjw  5126  nfdisj  5127  nfdisj1  5128  nfpo  5594  nfso  5595  nffr  5651  nfse  5652  nfwe  5653  nfrel  5780  sb8iota  6508  nffun  6572  nffn  6649  nff  6714  nff1  6786  nffo  6805  nff1o  6832  nfiso  7319  tz7.49  8445  nfixpw  8910  nfixp  8911  bnj919  33778  bnj1379  33841  bnj571  33917  bnj607  33927  bnj873  33935  bnj981  33961  bnj1039  33982  bnj1128  34001  bnj1388  34044  bnj1398  34045  bnj1417  34052  bnj1444  34054  bnj1445  34055  bnj1446  34056  bnj1449  34059  bnj1467  34065  bnj1489  34067  bnj1312  34069  bnj1518  34075  bnj1525  34080  wl-nfae1  36396  wl-ax11-lem4  36450  ptrecube  36488  nfdfat  45835  nfich1  46115  nfich2  46116  ichnfimlem  46131  ich2ex  46136