Theorem nfcxfr 2383

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

Syntax hints:   = wceq 1398   F/_wnfc 2373

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-cleq 2227  df-clel 2230  df-nfc 2375

This theorem is referenced by:  nfrab1  2726  nfrabw  2727  nfdif  3344  nfun  3379  nfin  3431  nfpw  3691  nfpr  3745  nfsn  3755  nfop  3905  nfuni  3926  nfint  3965  nfiunxy  4023  nfiinxy  4024  nfiunya  4025  nfiinya  4026  nfiu1  4027  nfii1  4028  nfopab  4184  nfopab1  4185  nfopab2  4186  nfmpt  4208  nfmpt1  4209  repizf2  4281  nfsuc  4535  nfxp  4782  nfco  4926  nfcnv  4940  nfdm  5007  nfrn  5008  nfres  5046  nfima  5115  nfiota1  5320  nffv  5686  fvmptss2  5758  fvmptssdm  5768  fvmptf  5776  ralrnmpt  5825  rexrnmpt  5826  f1ompt  5834  f1mpt  5951  fliftfun  5976  nfriota1  6020  riotaprop  6038  nfoprab1  6111  nfoprab2  6112  nfoprab3  6113  nfoprab  6114  nfmpo1  6129  nfmpo2  6130  nfmpo  6131  ovmpos  6186  ov2gf  6187  ovi3  6200  nfof  6282  nfofr  6283  nftpos  6524  nfrecs  6552  nffrec  6641  nfixpxy  6966  nfixp1  6967  xpcomco  7091  nfsup  7297  nfinf  7322  nfdju  7347  caucvgprprlemaddq  8040  nfseq  10847  nfwrd  11282  nfsum1  12071  nfsum  12072  nfcprod1  12270  nfcprod  12271  ballotfilem7  13228  lgseisenlem2  16075  lfgrnloopen  16259