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  2657  nfrabxy  2658  nfdif  3258  nfun  3293  nfin  3343  nfpw  3590  nfpr  3644  nfsn  3654  nfop  3796  nfuni  3817  nfint  3856  nfiunxy  3914  nfiinxy  3915  nfiunya  3916  nfiinya  3917  nfiu1  3918  nfii1  3919  nfopab  4073  nfopab1  4074  nfopab2  4075  nfmpt  4097  nfmpt1  4098  repizf2  4164  nfsuc  4410  nfxp  4655  nfco  4794  nfcnv  4808  nfdm  4873  nfrn  4874  nfres  4911  nfima  4980  nfiota1  5182  nffv  5527  fvmptss2  5594  fvmptssdm  5603  fvmptf  5611  ralrnmpt  5661  rexrnmpt  5662  f1ompt  5670  f1mpt  5775  fliftfun  5800  nfriota1  5841  riotaprop  5857  nfoprab1  5927  nfoprab2  5928  nfoprab3  5929  nfoprab  5930  nfmpo1  5945  nfmpo2  5946  nfmpo  5947  ovmpos  6001  ov2gf  6002  ovi3  6014  nfof  6091  nfofr  6092  nftpos  6283  nfrecs  6311  nffrec  6400  nfixpxy  6720  nfixp1  6721  xpcomco  6829  nfsup  6994  nfinf  7019  nfdju  7044  caucvgprprlemaddq  7710  nfseq  10458  nfsum1  11367  nfsum  11368  nfcprod1  11565  nfcprod  11566  lgseisenlem2  14639