Theorem nfcxfr 2383

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

Syntax hints:   = wceq 1398   F/_wnfc 2373

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-cleq 2227  df-clel 2230  df-nfc 2375

This theorem is referenced by:  nfrab1  2726  nfrabw  2727  nfdif  3344  nfun  3379  nfin  3431  nfpw  3690  nfpr  3744  nfsn  3754  nfop  3904  nfuni  3925  nfint  3964  nfiunxy  4022  nfiinxy  4023  nfiunya  4024  nfiinya  4025  nfiu1  4026  nfii1  4027  nfopab  4183  nfopab1  4184  nfopab2  4185  nfmpt  4207  nfmpt1  4208  repizf2  4280  nfsuc  4534  nfxp  4781  nfco  4925  nfcnv  4939  nfdm  5006  nfrn  5007  nfres  5045  nfima  5114  nfiota1  5319  nffv  5685  fvmptss2  5757  fvmptssdm  5767  fvmptf  5775  ralrnmpt  5824  rexrnmpt  5825  f1ompt  5833  f1mpt  5950  fliftfun  5975  nfriota1  6019  riotaprop  6037  nfoprab1  6110  nfoprab2  6111  nfoprab3  6112  nfoprab  6113  nfmpo1  6128  nfmpo2  6129  nfmpo  6130  ovmpos  6185  ov2gf  6186  ovi3  6199  nfof  6281  nfofr  6282  nftpos  6523  nfrecs  6551  nffrec  6640  nfixpxy  6965  nfixp1  6966  xpcomco  7090  nfsup  7296  nfinf  7321  nfdju  7346  caucvgprprlemaddq  8039  nfseq  10843  nfwrd  11278  nfsum1  12066  nfsum  12067  nfcprod1  12265  nfcprod  12266  ballotfilem7  13223  lgseisenlem2  16056  lfgrnloopen  16240