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  3280  nfun  3315  nfin  3365  nfpw  3614  nfpr  3668  nfsn  3678  nfop  3820  nfuni  3841  nfint  3880  nfiunxy  3938  nfiinxy  3939  nfiunya  3940  nfiinya  3941  nfiu1  3942  nfii1  3943  nfopab  4097  nfopab1  4098  nfopab2  4099  nfmpt  4121  nfmpt1  4122  repizf2  4191  nfsuc  4439  nfxp  4686  nfco  4827  nfcnv  4841  nfdm  4906  nfrn  4907  nfres  4944  nfima  5013  nfiota1  5217  nffv  5564  fvmptss2  5632  fvmptssdm  5642  fvmptf  5650  ralrnmpt  5700  rexrnmpt  5701  f1ompt  5709  f1mpt  5814  fliftfun  5839  nfriota1  5881  riotaprop  5897  nfoprab1  5967  nfoprab2  5968  nfoprab3  5969  nfoprab  5970  nfmpo1  5985  nfmpo2  5986  nfmpo  5987  ovmpos  6042  ov2gf  6043  ovi3  6055  nfof  6136  nfofr  6137  nftpos  6332  nfrecs  6360  nffrec  6449  nfixpxy  6771  nfixp1  6772  xpcomco  6880  nfsup  7051  nfinf  7076  nfdju  7101  caucvgprprlemaddq  7768  nfseq  10528  nfwrd  10942  nfsum1  11499  nfsum  11500  nfcprod1  11697  nfcprod  11698  lgseisenlem2  15187