Theorem nfcxfr 2975

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypotheses

Ref	Expression
nfcxfr.1	⊢ 𝐴 = 𝐵
nfcxfr.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfcxfr	⊢ Ⅎ𝑥𝐴

Proof of Theorem nfcxfr

Step	Hyp	Ref	Expression
1		nfcxfr.2	. 2 ⊢ Ⅎ𝑥𝐵
2		nfcxfr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	nfceqi 2973	. 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
4	1, 3	mpbir 233	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   = wceq 1537  Ⅎwnfc 2961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-cleq 2814  df-clel 2893  df-nfc 2963

This theorem is referenced by:  nfrab1  3384  nfrabw  3385  nfrab  3386  nfdif  4102  nfun  4141  nfin  4193  nfsymdif  4223  nfpw  4560  nfpr  4628  nfsn  4643  nfop  4819  nfint  4886  nfiun  4949  nfiin  4950  nfiung  4951  nfiing  4952  nfiu1  4953  nfii1  4954  nfopab  5134  nfopab1  5135  nfopab2  5136  nfmpt  5163  nfmpt1  5164  nfxp  5588  nfco  5736  nfcnv  5749  nfdm  5823  nfrn  5824  nfres  5855  nfima  5937  nfpred  6153  nfsuc  6262  nfiota1  6316  nffv  6680  fvmptss  6780  fvmptf  6789  fvopab5  6800  ralrnmptw  6860  ralrnmpt  6862  f1ompt  6875  f1mpt  7019  fliftfun  7065  nfriota1  7121  riotaprop  7141  nfoprab1  7215  nfoprab2  7216  nfoprab3  7217  nfoprab  7218  nfmpo1  7234  nfmpo2  7235  nfmpo  7236  ovmpos  7298  ov2gf  7299  ov3  7311  nfof  7414  nfofr  7415  nftpos  7927  fvmpocurryd  7937  nfwrecs  7949  nfrecs  8011  nfrdg  8050  rdgsucmptf  8064  rdgsucmptnf  8065  frsucmpt  8073  frsucmptn  8074  nfixpw  8480  nfixp  8481  nfixp1  8482  xpcomco  8607  nfsup  8915  nfinf  8946  nfoi  8978  cnfcom3clem  9168  nfdju  9336  dfac8clem  9458  iunfo  9961  pwfseqlem2  10081  pwfseqlem4a  10083  pwfseqlem4  10084  reclem2pr  10470  nfseq  13380  nfwrd  13894  nfsum1  15046  nfsumw  15047  nfsum  15048  nfcprod1  15264  nfcprod  15265  symgval  18497  ptbasfi  22189  mbfsup  24265  itg1climres  24315  itg2splitlem  24349  itg2split  24350  nfitg1  24374  nfitg  24375  lgamgulm2  25613  lgseisenlem2  25952  lfgrnloop  26910  numclwlk2lem2f1o  28158  cnlnadjlem5  29848  nfesum1  31299  nfesum2  31300  ballotlem7  31793  bnj1230  32074  bnj1476  32119  bnj900  32201  bnj958  32212  bnj1000  32213  bnj1014  32233  bnj1123  32258  bnj1307  32295  bnj1321  32299  bnj1384  32304  bnj1398  32306  bnj1408  32308  bnj1444  32315  bnj1445  32316  bnj1446  32317  bnj1447  32318  bnj1448  32319  bnj1449  32320  bnj1466  32325  bnj1467  32326  bnj1518  32336  bnj1519  32337  bnj1520  32338  bnj1525  32341  bnj1523  32343  cvmcov  32510  nfwsuc  33105  nfwlim  33109  nffrecs  33120  nosupbnd2  33216  nfaltop  33441  currysetlem1  34261  topdifinfindis  34630  rdgssun  34662  exrecfnlem  34663  finxpreclem6  34680  sdclem1  35033  riotasv2s  36109  cdleme26ee  37511  cdlemefs32sn1aw  37565  cdleme43fsv1snlem  37571  cdleme41sn3a  37584  cdleme32d  37595  cdleme32f  37597  cdleme40m  37618  cdleme40n  37619  ltrniotaval  37732  cdlemksv2  37998  cdlemkuv2  38018  cdlemk36  38064  cdlemk38  38066  cdlemkid  38087  cdlemk19x  38094  cdlemk11t  38097  areaquad  39843  nfscott  40595  nfcoll  40612  binomcxplemdvbinom  40705  binomcxplemdvsum  40707  binomcxplemnotnn0  40708  refsum2cnlem1  41314  eliuniincex  41395  suprnmpt  41450  disjrnmpt2  41469  fompt  41473  rnmptssbi  41554  allbutfi  41685  allbutfiinf  41714  fmuldfeqlem1  41883  fmuldfeq  41884  mullimc  41917  idlimc  41927  limcperiod  41929  neglimc  41948  addlimc  41949  0ellimcdiv  41950  fnlimcnv  41968  fnlimfvre  41975  fnlimfvre2  41978  fnlimf  41979  fnlimabslt  41980  xlimmnfmpt  42144  xlimpnfmpt  42145  cncfmptssg  42173  cncfshift  42177  cncficcgt0  42191  cncfiooicclem1  42196  dvnmul  42248  dvnprodlem1  42251  itgsinexplem1  42259  itgsubsticclem  42280  stoweidlem14  42319  stoweidlem16  42321  stoweidlem18  42323  stoweidlem22  42327  stoweidlem26  42331  stoweidlem27  42332  stoweidlem31  42336  stoweidlem32  42337  stoweidlem34  42339  stoweidlem35  42340  stoweidlem40  42345  stoweidlem41  42346  stoweidlem42  42347  stoweidlem44  42349  stoweidlem45  42350  stoweidlem46  42351  stoweidlem47  42352  stoweidlem48  42353  stoweidlem50  42355  stoweidlem51  42356  stoweidlem52  42357  stoweidlem53  42358  stoweidlem54  42359  stoweidlem57  42362  stoweidlem59  42364  stoweidlem62  42367  wallispilem5  42374  stirlinglem4  42382  stirlinglem5  42383  stirlinglem8  42386  stirlinglem11  42389  stirlinglem12  42390  stirlinglem13  42391  stirlinglem14  42392  stirlinglem15  42393  fourierdlem20  42432  fourierdlem31  42443  fourierdlem68  42479  fourierdlem80  42491  fourierdlem89  42500  fourierdlem91  42502  fourierdlem103  42514  fourierdlem104  42515  fourierdlem112  42523  fourierdlem115  42526  fourierd  42527  fourierclimd  42528  etransclem48  42587  iundjiun  42762  meaiuninc3v  42786  ovnlerp  42864  ovncvrrp  42866  ovnhoilem1  42903  opnvonmbllem1  42934  iunhoiioolem  42977  vonioo  42984  vonicc  42987  pimdecfgtioc  43013  pimincfltioc  43014  pimdecfgtioo  43015  pimincfltioo  43016  issmff  43031  incsmflem  43038  smfconst  43046  decsmflem  43062  smfpreimagtf  43064  smflimlem2  43068  smflim  43073  smfpimgtxr  43076  smfresal  43083  smfmullem2  43087  smfmullem4  43089  smfpimbor1lem2  43094  smflim2  43100  smfpimcclem  43101  smflimmpt  43104  smfsup  43108  smfsupmpt  43109  smfsupxr  43110  smfinf  43112  smfinfmpt  43113  smflimsuplem2  43115  smflimsuplem5  43118  smflimsup  43122  smfliminf  43125  nfafv  43355  nfaov  43398  nfafv2  43437  prmdvdsfmtnof1lem1  43766  nfsetrecs  44809