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  3588  nfpr  3642  nfsn  3652  nfop  3794  nfuni  3815  nfint  3854  nfiunxy  3912  nfiinxy  3913  nfiunya  3914  nfiinya  3915  nfiu1  3916  nfii1  3917  nfopab  4071  nfopab1  4072  nfopab2  4073  nfmpt  4095  nfmpt1  4096  repizf2  4162  nfsuc  4408  nfxp  4653  nfco  4792  nfcnv  4806  nfdm  4871  nfrn  4872  nfres  4909  nfima  4978  nfiota1  5180  nffv  5525  fvmptss2  5591  fvmptssdm  5600  fvmptf  5608  ralrnmpt  5658  rexrnmpt  5659  f1ompt  5667  f1mpt  5771  fliftfun  5796  nfriota1  5837  riotaprop  5853  nfoprab1  5923  nfoprab2  5924  nfoprab3  5925  nfoprab  5926  nfmpo1  5941  nfmpo2  5942  nfmpo  5943  ovmpos  5997  ov2gf  5998  ovi3  6010  nfof  6087  nfofr  6088  nftpos  6279  nfrecs  6307  nffrec  6396  nfixpxy  6716  nfixp1  6717  xpcomco  6825  nfsup  6990  nfinf  7015  nfdju  7040  caucvgprprlemaddq  7706  nfseq  10454  nfsum1  11363  nfsum  11364  nfcprod1  11561  nfcprod  11562  lgseisenlem2  14421