Theorem nfcxfr 2296

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

Syntax hints:   = wceq 1335   F/_wnfc 2286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-cleq 2150  df-clel 2153  df-nfc 2288

This theorem is referenced by:  nfrab1  2636  nfrabxy  2637  nfdif  3228  nfun  3263  nfin  3313  nfpw  3556  nfpr  3609  nfsn  3619  nfop  3757  nfuni  3778  nfint  3817  nfiunxy  3875  nfiinxy  3876  nfiunya  3877  nfiinya  3878  nfiu1  3879  nfii1  3880  nfopab  4032  nfopab1  4033  nfopab2  4034  nfmpt  4056  nfmpt1  4057  repizf2  4123  nfsuc  4368  nfxp  4613  nfco  4751  nfcnv  4765  nfdm  4830  nfrn  4831  nfres  4868  nfima  4936  nfiota1  5137  nffv  5478  fvmptss2  5543  fvmptssdm  5552  fvmptf  5560  ralrnmpt  5609  rexrnmpt  5610  f1ompt  5618  f1mpt  5721  fliftfun  5746  nfriota1  5787  riotaprop  5803  nfoprab1  5870  nfoprab2  5871  nfoprab3  5872  nfoprab  5873  nfmpo1  5888  nfmpo2  5889  nfmpo  5890  ovmpos  5944  ov2gf  5945  ovi3  5957  nfof  6037  nfofr  6038  nftpos  6226  nfrecs  6254  nffrec  6343  nfixpxy  6662  nfixp1  6663  xpcomco  6771  nfsup  6936  nfinf  6961  nfdju  6986  caucvgprprlemaddq  7628  nfseq  10354  nfsum1  11253  nfsum  11254  nfcprod1  11451  nfcprod  11452