Theorem nfcxfr 2924

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

Syntax hints:   = wceq 1562  Ⅎwnfc 2911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-nf 1806  df-cleq 2756  df-clel 2839  df-nfc 2913

This theorem is referenced by:  nfrab1  3436  nfrabw  3453  nfrab  3454  nfsymdif  4211  nfpw  4576  nfpr  4653  nfsn  4668  nfop  4849  nfint  4917  nfiun  4983  nfiin  4984  nfiung  4985  nfiing  4986  nfii1  4988  nfopab1  5172  nfopab2  5173  nfmpt  5200  nfmpt1  5201  nfxp  5682  nfco  5839  nfcnv  5852  nfdm  5929  nfrn  5930  nfres  5969  nfima  6059  nfpred  6295  nfsuc  6422  nfiota1  6481  nffv  6879  fvmptss  6990  fvmptf  6999  fvopab5  7011  ralrnmptw  7077  ralrnmpt  7079  f1ompt  7094  fompt  7101  f1mpt  7247  fliftfun  7298  nfriota1  7362  riotaprop  7382  nfoprab1  7459  nfoprab2  7460  nfoprab3  7461  nfoprab  7462  nfmpo1  7478  nfmpo2  7479  nfmpo  7480  ovmpos  7546  ov2gf  7547  ov3  7561  nfof  7668  nfofr  7669  nftpos  8243  fvmpocurryd  8253  nffrecs  8266  nfwrecs  8297  nfrecs  8347  nfrdg  8387  rdgsucmptf  8401  rdgsucmptnf  8402  frsucmpt  8411  frsucmptn  8412  nfixpw  8900  nfixp  8901  nfixp1  8902  xpcomco  9041  nfsup  9399  nfinf  9431  nfoi  9464  cnfcom3clem  9662  ttrclselem1  9682  ttrclselem2  9683  nfdju  9867  dfac8clem  9990  iunfo  10498  pwfseqlem2  10619  pwfseqlem4a  10621  pwfseqlem4  10622  reclem2pr  11008  nfseq  14026  nfwrd  14558  nfsum1  15719  nfsum  15720  nfcprod1  15940  nfcprod  15941  symgval  19413  ptbasfi  23643  mbfsup  25728  itg1climres  25778  itg2splitlem  25812  itg2split  25813  nfitg1  25838  nfitg  25839  lgamgulm2  27102  lgseisenlem2  27442  nosupbnd2  27782  noinfbnd2  27797  nfseqs  28382  lfgrnloop  29328  numclwlk2lem2f1o  30583  cnlnadjlem5  32276  2ndresdju  32853  nfesum1  34339  nfesum2  34340  ballotlem7  34835  bnj1230  35099  bnj1476  35144  bnj900  35226  bnj958  35237  bnj1000  35238  bnj1014  35258  bnj1123  35283  bnj1307  35320  bnj1321  35324  bnj1384  35329  bnj1398  35331  bnj1408  35333  bnj1444  35340  bnj1445  35341  bnj1446  35342  bnj1447  35343  bnj1448  35344  bnj1449  35345  bnj1466  35350  bnj1467  35351  bnj1518  35361  bnj1519  35362  bnj1520  35363  bnj1525  35366  bnj1523  35368  cvmcov  35618  nfwsuc  36171  nfwlim  36175  nfaltop  36335  nfttc  36856  currysetlem1  37437  topdifinfindis  37845  rdgssun  37877  exrecfnlem  37878  finxpreclem6  37895  sdclem1  38247  riotasv2s  39587  cdleme26ee  40989  cdlemefs32sn1aw  41043  cdleme43fsv1snlem  41049  cdleme41sn3a  41062  cdleme32d  41073  cdleme32f  41075  cdleme40m  41096  cdleme40n  41097  ltrniotaval  41210  cdlemksv2  41476  cdlemkuv2  41496  cdlemk36  41542  cdlemk38  41544  cdlemkid  41565  cdlemk19x  41572  cdlemk11t  41575  areaquad  43798  nfscott  44820  nfcoll  44837  binomcxplemdvbinom  44934  binomcxplemdvsum  44936  binomcxplemnotnn0  44937  refsum2cnlem1  45622  eliuniincex  45692  disjrnmpt2  45771  rnmptssbi  45840  allbutfi  45973  allbutfiinf  45999  rexanuz2nf  46071  fmuldfeqlem1  46163  fmuldfeq  46164  mullimc  46197  idlimc  46207  limcperiod  46209  neglimc  46226  addlimc  46227  0ellimcdiv  46228  fnlimcnv  46246  fnlimfvre  46253  fnlimfvre2  46256  fnlimf  46257  fnlimabslt  46258  xlimmnfmpt  46422  xlimpnfmpt  46423  cncfmptssg  46450  cncfshift  46453  cncficcgt0  46467  cncfiooicclem1  46472  dvnmul  46522  dvnprodlem1  46525  itgsinexplem1  46533  itgsubsticclem  46554  stoweidlem14  46593  stoweidlem16  46595  stoweidlem18  46597  stoweidlem22  46601  stoweidlem26  46605  stoweidlem27  46606  stoweidlem31  46610  stoweidlem32  46611  stoweidlem34  46613  stoweidlem35  46614  stoweidlem40  46619  stoweidlem41  46620  stoweidlem42  46621  stoweidlem44  46623  stoweidlem45  46624  stoweidlem46  46625  stoweidlem47  46626  stoweidlem48  46627  stoweidlem50  46629  stoweidlem51  46630  stoweidlem52  46631  stoweidlem53  46632  stoweidlem54  46633  stoweidlem57  46636  stoweidlem59  46638  stoweidlem62  46641  wallispilem5  46648  stirlinglem4  46656  stirlinglem5  46657  stirlinglem8  46660  stirlinglem11  46663  stirlinglem12  46664  stirlinglem13  46665  stirlinglem14  46666  stirlinglem15  46667  fourierdlem20  46706  fourierdlem31  46717  fourierdlem68  46753  fourierdlem80  46765  fourierdlem89  46774  fourierdlem91  46776  fourierdlem103  46788  fourierdlem104  46789  fourierdlem112  46797  fourierdlem115  46800  fourierd  46801  fourierclimd  46802  etransclem48  46861  iundjiun  47039  meaiuninc3v  47063  ovnlerp  47141  ovncvrrp  47143  ovnhoilem1  47180  opnvonmbllem1  47211  iunhoiioolem  47254  vonioo  47261  vonicc  47264  pimdecfgtioc  47294  pimincfltioc  47295  pimdecfgtioo  47296  pimincfltioo  47297  issmff  47313  incsmflem  47320  smfpimltxr  47326  smfconst  47328  decsmflem  47345  smfpreimagtf  47347  smflimlem2  47351  smflim  47356  smfpimgtxr  47359  smfresal  47367  smfmullem2  47371  smfmullem4  47373  smfpimbor1lem2  47378  smflim2  47385  smfpimcclem  47386  smflimmpt  47389  smfsup  47393  smfsupmpt  47394  smfsupxr  47395  smfinf  47397  smfinfmpt  47398  smflimsuplem2  47400  smflimsuplem5  47403  smflimsup  47407  smfliminf  47410  smfpimne2  47419  smfdivdmmbl2  47420  fsupdm  47421  fsupdm2  47422  finfdm  47425  finfdm2  47426  nfafv  47735  nfaov  47778  nfafv2  47817  prmdvdsfmtnof1lem1  48198  nfsetrecs  50312