Theorem nfcxfr 2369

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

Syntax hints:   = wceq 1395   F/_wnfc 2359

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-cleq 2222  df-clel 2225  df-nfc 2361

This theorem is referenced by:  nfrab1  2711  nfrabw  2712  nfdif  3325  nfun  3360  nfin  3410  nfpw  3662  nfpr  3716  nfsn  3726  nfop  3873  nfuni  3894  nfint  3933  nfiunxy  3991  nfiinxy  3992  nfiunya  3993  nfiinya  3994  nfiu1  3995  nfii1  3996  nfopab  4152  nfopab1  4153  nfopab2  4154  nfmpt  4176  nfmpt1  4177  repizf2  4247  nfsuc  4500  nfxp  4747  nfco  4890  nfcnv  4904  nfdm  4971  nfrn  4972  nfres  5010  nfima  5079  nfiota1  5283  nffv  5642  fvmptss2  5714  fvmptssdm  5724  fvmptf  5732  ralrnmpt  5782  rexrnmpt  5783  f1ompt  5791  f1mpt  5904  fliftfun  5929  nfriota1  5971  riotaprop  5989  nfoprab1  6062  nfoprab2  6063  nfoprab3  6064  nfoprab  6065  nfmpo1  6080  nfmpo2  6081  nfmpo  6082  ovmpos  6137  ov2gf  6138  ovi3  6151  nfof  6233  nfofr  6234  nftpos  6436  nfrecs  6464  nffrec  6553  nfixpxy  6877  nfixp1  6878  xpcomco  6998  nfsup  7175  nfinf  7200  nfdju  7225  caucvgprprlemaddq  7911  nfseq  10696  nfwrd  11118  nfsum1  11888  nfsum  11889  nfcprod1  12086  nfcprod  12087  lgseisenlem2  15771  lfgrnloopen  15952