Theorem nfcxfr 2922

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 2921	. 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
4	1, 3	mpbir 234	1 ⊢ Ⅎ𝑥𝐴

This proof depends on syntax axioms:   = wceq 1569  Ⅎwnfc 2909

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-nf 1813  df-cleq 2754  df-clel 2837  df-nfc 2911

This theorem is used by:  nfrab1  3435  nfrabw  3451  nfrab  3452  nfsymdif  4209  nfpw  4580  nfpr  4657  nfsn  4672  nfop  4853  nfint  4921  nfiun  4987  nfiin  4988  nfiung  4989  nfiing  4990  nfii1  4992  nfopab1  5180  nfopab2  5181  nfmpt  5208  nfmpt1  5209  nfxp  5693  nfco  5850  nfcnv  5863  nfdm  5940  nfrn  5941  nfres  5979  nfima  6069  nfpred  6307  nfsuc  6435  nfiota1  6494  nffv  6891  fvmptss  7002  fvmptf  7011  fvopab5  7023  ralrnmptw  7089  ralrnmpt  7091  f1ompt  7106  fompt  7113  f1mpt  7259  fliftfun  7310  nfriota1  7376  riotaprop  7396  nfoprab1  7473  nfoprab2  7474  nfoprab3  7475  nfoprab  7476  nfmpo1  7492  nfmpo2  7493  nfmpo  7494  ovmpos  7560  ov2gf  7561  ov3  7575  nfof  7682  nfofr  7683  nftpos  8255  fvmpocurryd  8265  nffrecs  8278  nfwrecs  8309  nfrecs  8359  nfrdg  8399  rdgsucmptf  8413  rdgsucmptnf  8414  frsucmpt  8423  frsucmptn  8424  nfixpw  8912  nfixp  8913  nfixp1  8914  xpcomco  9053  nfsup  9409  nfinf  9441  nfoi  9474  cnfcom3clem  9672  ttrclselem1  9692  ttrclselem2  9693  nfscott  9859  nfdju  9900  dfac8clem  10023  iunfo  10529  pwfseqlem2  10650  pwfseqlem4a  10652  pwfseqlem4  10653  reclem2pr  11039  nfseq  14054  nfwrd  14587  nfsum1  15748  nfsum  15749  nfcprod1  15969  nfcprod  15970  symgval  19447  ptbasfi  23749  mbfsup  25834  itg1climres  25884  itg2splitlem  25918  itg2split  25919  nfitg1  25944  nfitg  25945  lgamgulm2  27211  lgseisenlem2  27551  nosupbnd2  27891  noinfbnd2  27906  nfseqs  28491  lfgrnloop  29486  numclwlk2lem2f1o  30741  cnlnadjlem5  32434  2ndresdju  33005  nfesum1  34439  nfesum2  34440  ballotlem7  34935  bnj1230  35199  bnj1476  35244  bnj900  35326  bnj958  35337  bnj1000  35338  bnj1014  35358  bnj1123  35383  bnj1307  35420  bnj1321  35424  bnj1384  35429  bnj1398  35431  bnj1408  35433  bnj1444  35440  bnj1445  35441  bnj1446  35442  bnj1447  35443  bnj1448  35444  bnj1449  35445  bnj1466  35450  bnj1467  35451  bnj1518  35461  bnj1519  35462  bnj1520  35463  bnj1525  35466  bnj1523  35468  cvmcov  35763  nfwsuc  36316  nfwlim  36320  nfaltop  36480  nfttc  37030  currysetlem1  37611  topdifinfindis  38020  rdgssun  38052  exrecfnlem  38053  finxpreclem6  38070  sdclem1  38422  riotasv2s  39760  cdleme26ee  41162  cdlemefs32sn1aw  41216  cdleme43fsv1snlem  41222  cdleme41sn3a  41235  cdleme32d  41246  cdleme32f  41248  cdleme40m  41269  cdleme40n  41270  ltrniotaval  41383  cdlemksv2  41649  cdlemkuv2  41669  cdlemk36  41715  cdlemk38  41717  cdlemkid  41738  cdlemk19x  41745  cdlemk11t  41748  areaquad  43971  nfcoll  44994  binomcxplemdvbinom  45091  binomcxplemdvsum  45093  binomcxplemnotnn0  45094  refsum2cnlem1  45785  eliuniincex  45855  disjrnmpt2  45934  rnmptssbi  46003  allbutfi  46136  allbutfiinf  46162  rexanuz2nf  46234  fmuldfeqlem1  46326  fmuldfeq  46327  mullimc  46360  idlimc  46370  limcperiod  46372  neglimc  46389  addlimc  46390  0ellimcdiv  46391  fnlimcnv  46409  fnlimfvre  46416  fnlimfvre2  46419  fnlimf  46420  fnlimabslt  46421  xlimmnfmpt  46585  xlimpnfmpt  46586  cncfmptssg  46613  cncfshift  46616  cncficcgt0  46630  cncfiooicclem1  46635  dvnmul  46685  dvnprodlem1  46688  itgsinexplem1  46696  itgsubsticclem  46717  stoweidlem14  46756  stoweidlem16  46758  stoweidlem18  46760  stoweidlem22  46764  stoweidlem26  46768  stoweidlem27  46769  stoweidlem31  46773  stoweidlem32  46774  stoweidlem34  46776  stoweidlem35  46777  stoweidlem40  46782  stoweidlem41  46783  stoweidlem42  46784  stoweidlem44  46786  stoweidlem45  46787  stoweidlem46  46788  stoweidlem47  46789  stoweidlem48  46790  stoweidlem50  46792  stoweidlem51  46793  stoweidlem52  46794  stoweidlem53  46795  stoweidlem54  46796  stoweidlem57  46799  stoweidlem59  46801  stoweidlem62  46804  wallispilem5  46811  stirlinglem4  46819  stirlinglem5  46820  stirlinglem8  46823  stirlinglem11  46826  stirlinglem12  46827  stirlinglem13  46828  stirlinglem14  46829  stirlinglem15  46830  fourierdlem20  46869  fourierdlem31  46880  fourierdlem68  46916  fourierdlem80  46928  fourierdlem89  46937  fourierdlem91  46939  fourierdlem103  46951  fourierdlem104  46952  fourierdlem112  46960  fourierdlem115  46963  fourierd  46964  fourierclimd  46965  etransclem48  47024  iundjiun  47202  meaiuninc3v  47226  ovnlerp  47304  ovncvrrp  47306  ovnhoilem1  47343  opnvonmbllem1  47374  iunhoiioolem  47417  vonioo  47424  vonicc  47427  pimdecfgtioc  47457  pimincfltioc  47458  pimdecfgtioo  47459  pimincfltioo  47460  issmff  47476  incsmflem  47483  smfpimltxr  47489  smfconst  47491  decsmflem  47508  smfpreimagtf  47510  smflimlem2  47514  smflim  47519  smfpimgtxr  47522  smfresal  47530  smfmullem2  47534  smfmullem4  47536  smfpimbor1lem2  47541  smflim2  47548  smfpimcclem  47549  smflimmpt  47552  smfsup  47556  smfsupmpt  47557  smfsupxr  47558  smfinf  47560  smfinfmpt  47561  smflimsuplem2  47563  smflimsuplem5  47566  smflimsup  47570  smfliminf  47573  smfpimne2  47582  smfdivdmmbl2  47583  fsupdm  47584  fsupdm2  47585  finfdm  47588  finfdm2  47589  nfafv  47901  nfaov  47944  nfafv2  47983  prmdvdsfmtnof1lem1  48364  nfsetrecs  50492