Theorem nfcxfr 2389

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

This proof depends on syntax axioms:   = wceq 1402   F/_wnfc 2379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-cleq 2231  df-clel 2234  df-nfc 2381

This theorem is used by:  nfrab1  2732  nfrabw  2733  nfdif  3350  nfun  3385  nfin  3437  nfpw  3705  nfpr  3759  nfsn  3769  nfop  3920  nfuni  3941  nfint  3980  nfiunxy  4038  nfiinxy  4039  nfiunya  4040  nfiinya  4041  nfiu1  4042  nfii1  4043  nfopab  4200  nfopab1  4201  nfopab2  4202  nfmpt  4225  nfmpt1  4226  repizf2  4301  nfsuc  4555  nfxp  4803  nfco  4947  nfcnv  4961  nfdm  5028  nfrn  5029  nfres  5067  nfima  5137  nfiota1  5342  nffv  5708  fvmptss2  5783  fvmptssdm  5793  fvmptf  5801  ralrnmpt  5853  rexrnmpt  5854  f1ompt  5862  f1mpt  5980  fliftfun  6005  nfriota1  6049  riotaprop  6067  nfoprab1  6140  nfoprab2  6141  nfoprab3  6142  nfoprab  6143  nfmpo1  6158  nfmpo2  6159  nfmpo  6160  ovmpos  6215  ov2gf  6216  ovi3  6229  nfof  6312  nfofr  6313  nftpos  6554  nfrecs  6582  nffrec  6671  nfixpxy  7004  nfixp1  7005  xpcomco  7129  nfsup  7339  nfinf  7364  nfdju  7389  caucvgprprlemaddq  8082  nfseq  10916  nfwrd  11356  nfsum1  12148  nfsum  12149  nfcprod1  12347  nfcprod  12348  ballotfilem7  13338  lgseisenlem2  16407  lfgrnloopen  16591