Theorem nfcxfr 2316

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

Syntax hints:   = wceq 1353   F/_wnfc 2306

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-cleq 2170  df-clel 2173  df-nfc 2308

This theorem is referenced by:  nfrab1  2656  nfrabxy  2657  nfdif  3256  nfun  3291  nfin  3341  nfpw  3587  nfpr  3641  nfsn  3651  nfop  3792  nfuni  3813  nfint  3852  nfiunxy  3910  nfiinxy  3911  nfiunya  3912  nfiinya  3913  nfiu1  3914  nfii1  3915  nfopab  4068  nfopab1  4069  nfopab2  4070  nfmpt  4092  nfmpt1  4093  repizf2  4159  nfsuc  4405  nfxp  4650  nfco  4788  nfcnv  4802  nfdm  4867  nfrn  4868  nfres  4905  nfima  4974  nfiota1  5176  nffv  5521  fvmptss2  5587  fvmptssdm  5596  fvmptf  5604  ralrnmpt  5654  rexrnmpt  5655  f1ompt  5663  f1mpt  5766  fliftfun  5791  nfriota1  5832  riotaprop  5848  nfoprab1  5918  nfoprab2  5919  nfoprab3  5920  nfoprab  5921  nfmpo1  5936  nfmpo2  5937  nfmpo  5938  ovmpos  5992  ov2gf  5993  ovi3  6005  nfof  6082  nfofr  6083  nftpos  6274  nfrecs  6302  nffrec  6391  nfixpxy  6711  nfixp1  6712  xpcomco  6820  nfsup  6985  nfinf  7010  nfdju  7035  caucvgprprlemaddq  7698  nfseq  10441  nfsum1  11348  nfsum  11349  nfcprod1  11546  nfcprod  11547