Theorem nfcxfr 2333

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

Syntax hints:   = wceq 1364   F/_wnfc 2323

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-cleq 2186  df-clel 2189  df-nfc 2325

This theorem is referenced by:  nfrab1  2674  nfrabw  2675  nfdif  3281  nfun  3316  nfin  3366  nfpw  3615  nfpr  3669  nfsn  3679  nfop  3821  nfuni  3842  nfint  3881  nfiunxy  3939  nfiinxy  3940  nfiunya  3941  nfiinya  3942  nfiu1  3943  nfii1  3944  nfopab  4098  nfopab1  4099  nfopab2  4100  nfmpt  4122  nfmpt1  4123  repizf2  4192  nfsuc  4440  nfxp  4687  nfco  4828  nfcnv  4842  nfdm  4907  nfrn  4908  nfres  4945  nfima  5014  nfiota1  5218  nffv  5565  fvmptss2  5633  fvmptssdm  5643  fvmptf  5651  ralrnmpt  5701  rexrnmpt  5702  f1ompt  5710  f1mpt  5815  fliftfun  5840  nfriota1  5882  riotaprop  5898  nfoprab1  5968  nfoprab2  5969  nfoprab3  5970  nfoprab  5971  nfmpo1  5986  nfmpo2  5987  nfmpo  5988  ovmpos  6043  ov2gf  6044  ovi3  6057  nfof  6138  nfofr  6139  nftpos  6334  nfrecs  6362  nffrec  6451  nfixpxy  6773  nfixp1  6774  xpcomco  6882  nfsup  7053  nfinf  7078  nfdju  7103  caucvgprprlemaddq  7770  nfseq  10531  nfwrd  10945  nfsum1  11502  nfsum  11503  nfcprod1  11700  nfcprod  11701  lgseisenlem2  15228