Theorem nfcxfr 2762

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

Syntax hints:   = wceq 1483   F/_wnfc 2751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-clel 2618  df-nfc 2753

This theorem is referenced by:  nfrab1  3122  nfrab  3123  nfdif  3731  nfun  3769  nfin  3820  nfsymdif  3848  nfpw  4172  nfpr  4232  nfsn  4242  nfop  4418  nfuni  4442  nfint  4486  nfiun  4548  nfiin  4549  nfiu1  4550  nfii1  4551  nfopab  4718  nfopab1  4719  nfopab2  4720  nfmpt  4746  nfmpt1  4747  nfxp  5142  nfco  5287  nfcnv  5301  nfdm  5367  nfrn  5368  nfres  5398  nfima  5474  nfpred  5685  nfsuc  5796  nfiota1  5853  nffv  6198  fvmptss  6292  fvmptf  6301  fvopab5  6309  ralrnmpt  6368  f1ompt  6382  f1mpt  6518  fliftfun  6562  nfriota1  6618  riotaprop  6635  nfoprab1  6704  nfoprab2  6705  nfoprab3  6706  nfoprab  6707  nfmpt21  6722  nfmpt22  6723  nfmpt2  6724  ovmpt2s  6784  ov2gf  6785  ov3  6797  nftpos  7387  fvmpt2curryd  7397  nfwrecs  7409  nfrecs  7471  nfrdg  7510  rdgsucmptf  7524  rdgsucmptnf  7525  frsucmpt  7533  frsucmptn  7534  nfixp  7927  nfixp1  7928  xpcomco  8050  nfsup  8357  nfinf  8388  nfoi  8419  cnfcom3clem  8602  dfac8clem  8855  iunfo  9361  pwfseqlem2  9481  pwfseqlem4a  9483  pwfseqlem4  9484  reclem2pr  9870  nfseq  12811  nfwrd  13333  nfsum1  14420  nfsum  14421  nfcprod1  14640  nfcprod  14641  ptbasfi  21384  mbfsup  23431  itg1climres  23481  itg2splitlem  23515  itg2split  23516  nfitg1  23540  nfitg  23541  lgamgulm2  24762  lgseisenlem2  25101  lfgrnloop  26020  numclwlk1lem2  27230  numclwlk2lem2f1o  27238  cnlnadjlem5  28930  nfesum1  30102  nfesum2  30103  ballotlem7  30597  bnj1230  30873  bnj1476  30917  bnj900  30999  bnj958  31010  bnj1000  31011  bnj1014  31030  bnj1123  31054  bnj1307  31091  bnj1321  31095  bnj1384  31100  bnj1398  31102  bnj1408  31104  bnj1444  31111  bnj1445  31112  bnj1446  31113  bnj1447  31114  bnj1448  31115  bnj1449  31116  bnj1466  31121  bnj1467  31122  bnj1518  31132  bnj1519  31133  bnj1520  31134  bnj1525  31137  bnj1523  31139  cvmcov  31245  nfwsuc  31764  nfwlim  31768  nosupbnd2  31862  nfaltop  32087  topdifinfindis  33194  finxpreclem6  33233  sdclem1  33539  riotasv2s  34244  cdleme26ee  35648  cdlemefs32sn1aw  35702  cdleme43fsv1snlem  35708  cdleme41sn3a  35721  cdleme32d  35732  cdleme32f  35734  cdleme40m  35755  cdleme40n  35756  ltrniotaval  35869  cdlemksv2  36135  cdlemkuv2  36155  cdlemk36  36201  cdlemk38  36203  cdlemkid  36224  cdlemk19x  36231  cdlemk11t  36234  areaquad  37802  binomcxplemdvbinom  38552  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  refsum2cnlem1  39196  eliuniincex  39292  suprnmpt  39355  wessf1ornlem  39371  disjrnmpt2  39375  fompt  39379  rnmptssbi  39477  allbutfi  39616  allbutfiinf  39647  fmuldfeqlem1  39814  fmuldfeq  39815  mullimc  39848  idlimc  39858  limcperiod  39860  neglimc  39879  addlimc  39880  0ellimcdiv  39881  fnlimcnv  39899  fnlimfvre  39906  fnlimfvre2  39909  fnlimf  39910  fnlimabslt  39911  xlimmnfmpt  40069  xlimpnfmpt  40070  cncfmptssg  40083  cncfshift  40087  cncficcgt0  40101  cncfiooicclem1  40106  dvnmul  40158  dvnprodlem1  40161  itgsinexplem1  40169  itgsubsticclem  40191  stoweidlem14  40231  stoweidlem16  40233  stoweidlem18  40235  stoweidlem22  40239  stoweidlem26  40243  stoweidlem27  40244  stoweidlem31  40248  stoweidlem32  40249  stoweidlem34  40251  stoweidlem35  40252  stoweidlem40  40257  stoweidlem41  40258  stoweidlem42  40259  stoweidlem44  40261  stoweidlem45  40262  stoweidlem46  40263  stoweidlem47  40264  stoweidlem48  40265  stoweidlem50  40267  stoweidlem51  40268  stoweidlem52  40269  stoweidlem53  40270  stoweidlem54  40271  stoweidlem57  40274  stoweidlem59  40276  stoweidlem62  40279  wallispilem5  40286  stirlinglem4  40294  stirlinglem5  40295  stirlinglem8  40298  stirlinglem11  40301  stirlinglem12  40302  stirlinglem13  40303  stirlinglem14  40304  stirlinglem15  40305  fourierdlem20  40344  fourierdlem31  40355  fourierdlem68  40391  fourierdlem80  40403  fourierdlem89  40412  fourierdlem91  40414  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fourierdlem115  40438  fourierd  40439  fourierclimd  40440  etransclem48  40499  iundjiun  40677  ovnlerp  40776  ovncvrrp  40778  ovnhoilem1  40815  opnvonmbllem1  40846  iunhoiioolem  40889  vonioo  40896  vonicc  40899  pimdecfgtioc  40925  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  issmff  40943  incsmflem  40950  smfconst  40958  decsmflem  40974  smfpreimagtf  40976  smflimlem2  40980  smflim  40985  smfpimgtxr  40988  smfresal  40995  smfmullem2  40999  smfmullem4  41001  smfpimbor1lem2  41006  smflim2  41012  smfpimcclem  41013  smflimmpt  41016  smfsup  41020  smfsupmpt  41021  smfsupxr  41022  smfinf  41024  smfinfmpt  41025  smflimsuplem2  41027  smflimsuplem5  41030  smflimsup  41034  smfliminf  41037  nfafv  41216  nfaov  41259  prmdvdsfmtnof1lem1  41496  nfsetrecs  42433