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  3257  nfun  3292  nfin  3342  nfpw  3589  nfpr  3643  nfsn  3653  nfop  3795  nfuni  3816  nfint  3855  nfiunxy  3913  nfiinxy  3914  nfiunya  3915  nfiinya  3916  nfiu1  3917  nfii1  3918  nfopab  4072  nfopab1  4073  nfopab2  4074  nfmpt  4096  nfmpt1  4097  repizf2  4163  nfsuc  4409  nfxp  4654  nfco  4793  nfcnv  4807  nfdm  4872  nfrn  4873  nfres  4910  nfima  4979  nfiota1  5181  nffv  5526  fvmptss2  5592  fvmptssdm  5601  fvmptf  5609  ralrnmpt  5659  rexrnmpt  5660  f1ompt  5668  f1mpt  5772  fliftfun  5797  nfriota1  5838  riotaprop  5854  nfoprab1  5924  nfoprab2  5925  nfoprab3  5926  nfoprab  5927  nfmpo1  5942  nfmpo2  5943  nfmpo  5944  ovmpos  5998  ov2gf  5999  ovi3  6011  nfof  6088  nfofr  6089  nftpos  6280  nfrecs  6308  nffrec  6397  nfixpxy  6717  nfixp1  6718  xpcomco  6826  nfsup  6991  nfinf  7016  nfdju  7041  caucvgprprlemaddq  7707  nfseq  10455  nfsum1  11364  nfsum  11365  nfcprod1  11562  nfcprod  11563  lgseisenlem2  14454