Theorem nfcxfr 2371

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

Hypotheses

Ref	Expression
nfceqi.1	|- A = B
nfcxfr.2	|- F/_ x B

Assertion

Ref	Expression
nfcxfr	|- F/_ x A

Proof of Theorem nfcxfr

Step	Hyp	Ref	Expression
1		nfcxfr.2	. 2 |- F/_ x B
2		nfceqi.1	. . 3 |- A = B
3	2	nfceqi 2370	. 2 |- ( F/_ x A <-> F/_ x B )
4	1, 3	mpbir 146	1 |- F/_ x A

Syntax hints:   = wceq 1397   F/_wnfc 2361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-cleq 2224  df-clel 2227  df-nfc 2363

This theorem is referenced by:  nfrab1  2713  nfrabw  2714  nfdif  3328  nfun  3363  nfin  3413  nfpw  3665  nfpr  3719  nfsn  3729  nfop  3878  nfuni  3899  nfint  3938  nfiunxy  3996  nfiinxy  3997  nfiunya  3998  nfiinya  3999  nfiu1  4000  nfii1  4001  nfopab  4157  nfopab1  4158  nfopab2  4159  nfmpt  4181  nfmpt1  4182  repizf2  4252  nfsuc  4505  nfxp  4752  nfco  4895  nfcnv  4909  nfdm  4976  nfrn  4977  nfres  5015  nfima  5084  nfiota1  5288  nffv  5649  fvmptss2  5721  fvmptssdm  5731  fvmptf  5739  ralrnmpt  5789  rexrnmpt  5790  f1ompt  5798  f1mpt  5912  fliftfun  5937  nfriota1  5979  riotaprop  5997  nfoprab1  6070  nfoprab2  6071  nfoprab3  6072  nfoprab  6073  nfmpo1  6088  nfmpo2  6089  nfmpo  6090  ovmpos  6145  ov2gf  6146  ovi3  6159  nfof  6241  nfofr  6242  nftpos  6445  nfrecs  6473  nffrec  6562  nfixpxy  6886  nfixp1  6887  xpcomco  7010  nfsup  7191  nfinf  7216  nfdju  7241  caucvgprprlemaddq  7928  nfseq  10720  nfwrd  11146  nfsum1  11921  nfsum  11922  nfcprod1  12120  nfcprod  12121  lgseisenlem2  15806  lfgrnloopen  15990