MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfcxfr Structured version   Visualization version   GIF version

Theorem nfcxfr 2791
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 𝐴 = 𝐵
nfcxfr.2 𝑥𝐵
Assertion
Ref Expression
nfcxfr 𝑥𝐴

Proof of Theorem nfcxfr
StepHypRef Expression
1 nfcxfr.2 . 2 𝑥𝐵
2 nfceqi.1 . . 3 𝐴 = 𝐵
32nfceqi 2790 . 2 (𝑥𝐴𝑥𝐵)
41, 3mpbir 221 1 𝑥𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wnfc 2780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-clel 2647  df-nfc 2782
This theorem is referenced by:  nfrab1  3152  nfrab  3153  nfdif  3764  nfun  3802  nfin  3853  nfsymdif  3881  nfpw  4205  nfpr  4264  nfsn  4274  nfop  4449  nfuni  4474  nfint  4518  nfiun  4580  nfiin  4581  nfiu1  4582  nfii1  4583  nfopab  4751  nfopab1  4752  nfopab2  4753  nfmpt  4779  nfmpt1  4780  nfxp  5176  nfco  5320  nfcnv  5333  nfdm  5399  nfrn  5400  nfres  5430  nfima  5509  nfpred  5723  nfsuc  5834  nfiota1  5891  nffv  6236  fvmptss  6331  fvmptf  6340  fvopab5  6349  ralrnmpt  6408  f1ompt  6422  f1mpt  6558  fliftfun  6602  nfriota1  6658  riotaprop  6675  nfoprab1  6746  nfoprab2  6747  nfoprab3  6748  nfoprab  6749  nfmpt21  6764  nfmpt22  6765  nfmpt2  6766  ovmpt2s  6826  ov2gf  6827  ov3  6839  nftpos  7432  fvmpt2curryd  7442  nfwrecs  7454  nfrecs  7516  nfrdg  7555  rdgsucmptf  7569  rdgsucmptnf  7570  frsucmpt  7578  frsucmptn  7579  nfixp  7969  nfixp1  7970  xpcomco  8091  nfsup  8398  nfinf  8429  nfoi  8460  cnfcom3clem  8640  dfac8clem  8893  iunfo  9399  pwfseqlem2  9519  pwfseqlem4a  9521  pwfseqlem4  9522  reclem2pr  9908  nfseq  12851  nfwrd  13365  nfsum1  14464  nfsum  14465  nfcprod1  14684  nfcprod  14685  ptbasfi  21432  mbfsup  23476  itg1climres  23526  itg2splitlem  23560  itg2split  23561  nfitg1  23585  nfitg  23586  lgamgulm2  24807  lgseisenlem2  25146  lfgrnloop  26065  numclwlk1lem2  27350  numclwlk2lem2f1o  27359  numclwlk2lem2f1oOLD  27366  cnlnadjlem5  29058  nfesum1  30230  nfesum2  30231  ballotlem7  30725  bnj1230  30999  bnj1476  31043  bnj900  31125  bnj958  31136  bnj1000  31137  bnj1014  31156  bnj1123  31180  bnj1307  31217  bnj1321  31221  bnj1384  31226  bnj1398  31228  bnj1408  31230  bnj1444  31237  bnj1445  31238  bnj1446  31239  bnj1447  31240  bnj1448  31241  bnj1449  31242  bnj1466  31247  bnj1467  31248  bnj1518  31258  bnj1519  31259  bnj1520  31260  bnj1525  31263  bnj1523  31265  cvmcov  31371  nfwsuc  31888  nfwlim  31892  nffrecs  31903  nosupbnd2  31987  nfaltop  32212  topdifinfindis  33324  finxpreclem6  33363  sdclem1  33669  riotasv2s  34562  cdleme26ee  35965  cdlemefs32sn1aw  36019  cdleme43fsv1snlem  36025  cdleme41sn3a  36038  cdleme32d  36049  cdleme32f  36051  cdleme40m  36072  cdleme40n  36073  ltrniotaval  36186  cdlemksv2  36452  cdlemkuv2  36472  cdlemk36  36518  cdlemk38  36520  cdlemkid  36541  cdlemk19x  36548  cdlemk11t  36551  areaquad  38119  binomcxplemdvbinom  38869  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  refsum2cnlem1  39510  eliuniincex  39606  suprnmpt  39669  wessf1ornlem  39685  disjrnmpt2  39689  fompt  39693  rnmptssbi  39791  allbutfi  39929  allbutfiinf  39960  fmuldfeqlem1  40132  fmuldfeq  40133  mullimc  40166  idlimc  40176  limcperiod  40178  neglimc  40197  addlimc  40198  0ellimcdiv  40199  fnlimcnv  40217  fnlimfvre  40224  fnlimfvre2  40227  fnlimf  40228  fnlimabslt  40229  xlimmnfmpt  40387  xlimpnfmpt  40388  cncfmptssg  40401  cncfshift  40405  cncficcgt0  40419  cncfiooicclem1  40424  dvnmul  40476  dvnprodlem1  40479  itgsinexplem1  40487  itgsubsticclem  40509  stoweidlem14  40549  stoweidlem16  40551  stoweidlem18  40553  stoweidlem22  40557  stoweidlem26  40561  stoweidlem27  40562  stoweidlem31  40566  stoweidlem32  40567  stoweidlem34  40569  stoweidlem35  40570  stoweidlem40  40575  stoweidlem41  40576  stoweidlem42  40577  stoweidlem44  40579  stoweidlem45  40580  stoweidlem46  40581  stoweidlem47  40582  stoweidlem48  40583  stoweidlem50  40585  stoweidlem51  40586  stoweidlem52  40587  stoweidlem53  40588  stoweidlem54  40589  stoweidlem57  40592  stoweidlem59  40594  stoweidlem62  40597  wallispilem5  40604  stirlinglem4  40612  stirlinglem5  40613  stirlinglem8  40616  stirlinglem11  40619  stirlinglem12  40620  stirlinglem13  40621  stirlinglem14  40622  stirlinglem15  40623  fourierdlem20  40662  fourierdlem31  40673  fourierdlem68  40709  fourierdlem80  40721  fourierdlem89  40730  fourierdlem91  40732  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  fourierdlem115  40756  fourierd  40757  fourierclimd  40758  etransclem48  40817  iundjiun  40995  meaiuninc3v  41019  ovnlerp  41097  ovncvrrp  41099  ovnhoilem1  41136  opnvonmbllem1  41167  iunhoiioolem  41210  vonioo  41217  vonicc  41220  pimdecfgtioc  41246  pimincfltioc  41247  pimdecfgtioo  41248  pimincfltioo  41249  issmff  41264  incsmflem  41271  smfconst  41279  decsmflem  41295  smfpreimagtf  41297  smflimlem2  41301  smflim  41306  smfpimgtxr  41309  smfresal  41316  smfmullem2  41320  smfmullem4  41322  smfpimbor1lem2  41327  smflim2  41333  smfpimcclem  41334  smflimmpt  41337  smfsup  41341  smfsupmpt  41342  smfsupxr  41343  smfinf  41345  smfinfmpt  41346  smflimsuplem2  41348  smflimsuplem5  41351  smflimsup  41355  smfliminf  41358  nfafv  41537  nfaov  41580  prmdvdsfmtnof1lem1  41821  nfsetrecs  42758
  Copyright terms: Public domain W3C validator