Theorem nfcxfr 2309

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 2308	. 2 |- ( F/_ x A <-> F/_ x B )
4	1, 3	mpbir 145	1 |- F/_ x A

Syntax hints:   = wceq 1348   F/_wnfc 2299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-cleq 2163  df-clel 2166  df-nfc 2301

This theorem is referenced by:  nfrab1  2649  nfrabxy  2650  nfdif  3248  nfun  3283  nfin  3333  nfpw  3579  nfpr  3633  nfsn  3643  nfop  3781  nfuni  3802  nfint  3841  nfiunxy  3899  nfiinxy  3900  nfiunya  3901  nfiinya  3902  nfiu1  3903  nfii1  3904  nfopab  4057  nfopab1  4058  nfopab2  4059  nfmpt  4081  nfmpt1  4082  repizf2  4148  nfsuc  4393  nfxp  4638  nfco  4776  nfcnv  4790  nfdm  4855  nfrn  4856  nfres  4893  nfima  4961  nfiota1  5162  nffv  5506  fvmptss2  5571  fvmptssdm  5580  fvmptf  5588  ralrnmpt  5638  rexrnmpt  5639  f1ompt  5647  f1mpt  5750  fliftfun  5775  nfriota1  5816  riotaprop  5832  nfoprab1  5902  nfoprab2  5903  nfoprab3  5904  nfoprab  5905  nfmpo1  5920  nfmpo2  5921  nfmpo  5922  ovmpos  5976  ov2gf  5977  ovi3  5989  nfof  6066  nfofr  6067  nftpos  6258  nfrecs  6286  nffrec  6375  nfixpxy  6695  nfixp1  6696  xpcomco  6804  nfsup  6969  nfinf  6994  nfdju  7019  caucvgprprlemaddq  7670  nfseq  10411  nfsum1  11319  nfsum  11320  nfcprod1  11517  nfcprod  11518