Theorem nfcxfr 2345

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

Syntax hints:   = wceq 1373   F/_wnfc 2335

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-cleq 2198  df-clel 2201  df-nfc 2337

This theorem is referenced by:  nfrab1  2686  nfrabw  2687  nfdif  3294  nfun  3329  nfin  3379  nfpw  3629  nfpr  3683  nfsn  3693  nfop  3835  nfuni  3856  nfint  3895  nfiunxy  3953  nfiinxy  3954  nfiunya  3955  nfiinya  3956  nfiu1  3957  nfii1  3958  nfopab  4113  nfopab1  4114  nfopab2  4115  nfmpt  4137  nfmpt1  4138  repizf2  4207  nfsuc  4456  nfxp  4703  nfco  4844  nfcnv  4858  nfdm  4923  nfrn  4924  nfres  4962  nfima  5031  nfiota1  5235  nffv  5588  fvmptss2  5656  fvmptssdm  5666  fvmptf  5674  ralrnmpt  5724  rexrnmpt  5725  f1ompt  5733  f1mpt  5842  fliftfun  5867  nfriota1  5909  riotaprop  5925  nfoprab1  5996  nfoprab2  5997  nfoprab3  5998  nfoprab  5999  nfmpo1  6014  nfmpo2  6015  nfmpo  6016  ovmpos  6071  ov2gf  6072  ovi3  6085  nfof  6166  nfofr  6167  nftpos  6367  nfrecs  6395  nffrec  6484  nfixpxy  6806  nfixp1  6807  xpcomco  6923  nfsup  7096  nfinf  7121  nfdju  7146  caucvgprprlemaddq  7823  nfseq  10604  nfwrd  11024  nfsum1  11700  nfsum  11701  nfcprod1  11898  nfcprod  11899  lgseisenlem2  15581