Theorem nfcxfr 2389

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

Syntax hints:   = wceq 1402   F/_wnfc 2379

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-cleq 2231  df-clel 2234  df-nfc 2381

This theorem is referenced by:  nfrab1  2732  nfrabw  2733  nfdif  3350  nfun  3385  nfin  3437  nfpw  3704  nfpr  3758  nfsn  3768  nfop  3918  nfuni  3939  nfint  3978  nfiunxy  4036  nfiinxy  4037  nfiunya  4038  nfiinya  4039  nfiu1  4040  nfii1  4041  nfopab  4197  nfopab1  4198  nfopab2  4199  nfmpt  4221  nfmpt1  4222  repizf2  4297  nfsuc  4551  nfxp  4799  nfco  4943  nfcnv  4957  nfdm  5024  nfrn  5025  nfres  5063  nfima  5132  nfiota1  5337  nffv  5703  fvmptss2  5777  fvmptssdm  5787  fvmptf  5795  ralrnmpt  5844  rexrnmpt  5845  f1ompt  5853  f1mpt  5971  fliftfun  5996  nfriota1  6040  riotaprop  6058  nfoprab1  6131  nfoprab2  6132  nfoprab3  6133  nfoprab  6134  nfmpo1  6149  nfmpo2  6150  nfmpo  6151  ovmpos  6206  ov2gf  6207  ovi3  6220  nfof  6302  nfofr  6303  nftpos  6544  nfrecs  6572  nffrec  6661  nfixpxy  6993  nfixp1  6994  xpcomco  7118  nfsup  7326  nfinf  7351  nfdju  7376  caucvgprprlemaddq  8069  nfseq  10877  nfwrd  11316  nfsum1  12105  nfsum  12106  nfcprod1  12304  nfcprod  12305  ballotfilem7  13262  lgseisenlem2  16173  lfgrnloopen  16357