Theorem nfcxfr 2381

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

Syntax hints:   = wceq 1398   F/_wnfc 2371

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-cleq 2225  df-clel 2228  df-nfc 2373

This theorem is referenced by:  nfrab1  2723  nfrabw  2724  nfdif  3339  nfun  3374  nfin  3426  nfpw  3684  nfpr  3738  nfsn  3748  nfop  3898  nfuni  3919  nfint  3958  nfiunxy  4016  nfiinxy  4017  nfiunya  4018  nfiinya  4019  nfiu1  4020  nfii1  4021  nfopab  4177  nfopab1  4178  nfopab2  4179  nfmpt  4201  nfmpt1  4202  repizf2  4274  nfsuc  4528  nfxp  4775  nfco  4919  nfcnv  4933  nfdm  5000  nfrn  5001  nfres  5039  nfima  5108  nfiota1  5313  nffv  5679  fvmptss2  5751  fvmptssdm  5761  fvmptf  5769  ralrnmpt  5818  rexrnmpt  5819  f1ompt  5827  f1mpt  5943  fliftfun  5968  nfriota1  6010  riotaprop  6028  nfoprab1  6101  nfoprab2  6102  nfoprab3  6103  nfoprab  6104  nfmpo1  6119  nfmpo2  6120  nfmpo  6121  ovmpos  6176  ov2gf  6177  ovi3  6190  nfof  6271  nfofr  6272  nftpos  6509  nfrecs  6537  nffrec  6626  nfixpxy  6951  nfixp1  6952  xpcomco  7076  nfsup  7282  nfinf  7307  nfdju  7332  caucvgprprlemaddq  8022  nfseq  10818  nfwrd  11249  nfsum1  12037  nfsum  12038  nfcprod1  12236  nfcprod  12237  lgseisenlem2  15936  lfgrnloopen  16120