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

Theorem nfcxfr 2617
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 2615 . 2
41, 3mpbir 209 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  F/_wnfc 2605
This theorem is referenced by:  nfrab1  3038  nfrab  3039  nfdif  3624  nfun  3659  nfin  3704  nfpw  4024  nfpr  4076  nfsn  4087  nfop  4233  nfuni  4255  nfint  4296  nfiun  4358  nfiin  4359  nfiu1  4360  nfii1  4361  nfopab  4517  nfopab1  4518  nfopab2  4519  nfmpt  4540  nfmpt1  4541  nfsuc  4954  nfxp  5031  nfco  5173  nfcnv  5186  nfdm  5249  nfrn  5250  nfres  5280  nfima  5350  nfiota1  5558  nffv  5878  fvmptss  5964  fvmptf  5972  fvopab5  5979  ralrnmpt  6040  f1ompt  6053  f1mpt  6169  fliftfun  6210  nfriota1  6264  riotaprop  6281  nfoprab1  6346  nfoprab2  6347  nfoprab3  6348  nfoprab  6349  nfmpt21  6364  nfmpt22  6365  nfmpt2  6366  ovmpt2s  6426  ov2gf  6427  ov3  6439  nftpos  7009  fvmpt2curryd  7019  nfrecs  7063  nfrdg  7099  rdgsucmptf  7113  rdgsucmptnf  7114  frsucmpt  7122  frsucmptn  7123  nfixp  7508  nfixp1  7509  xpcomco  7627  nfsup  7931  nfoi  7960  cnfcom3clem  8170  cnfcom3clemOLD  8178  dfac8clem  8434  iunfo  8935  pwfseqlem2  9058  pwfseqlem4a  9060  pwfseqlem4  9061  reclem2pr  9447  nfseq  12117  nfwrd  12569  nfsum1  13512  nfsum  13513  nfcprod1  13717  nfcprod  13718  ptbasfi  20082  mbfsup  22071  itg1climres  22121  itg2splitlem  22155  itg2split  22156  nfitg1  22180  nfitg  22181  lgseisenlem2  23625  cnlnadjlem5  26990  nfesum1  28053  ballotlem7  28474  lgamgulm2  28578  cvmcov  28708  nfpred  29249  nfwrecs  29338  nfwsuc  29374  nfwlim  29378  nfsymdif  29472  nfaltop  29630  sdclem1  30236  areaquad  31184  binomcxplemdvbinom  31258  binomcxplemdvsum  31260  binomcxplemnotnn0  31261  refsum2cnlem1  31412  suprnmpt  31451  fmuldfeqlem1  31576  fmuldfeq  31577  mullimc  31622  idlimc  31632  limcperiod  31634  neglimc  31653  addlimc  31654  0ellimcdiv  31655  cncfmptssg  31672  cncfshift  31676  cncficcgt0  31691  cncfiooicclem1  31696  dvnmul  31740  dvnprodlem1  31743  itgsinexplem1  31752  itgsubsticclem  31774  stoweidlem14  31796  stoweidlem16  31798  stoweidlem18  31800  stoweidlem22  31804  stoweidlem26  31808  stoweidlem27  31809  stoweidlem31  31813  stoweidlem32  31814  stoweidlem34  31816  stoweidlem35  31817  stoweidlem40  31822  stoweidlem41  31823  stoweidlem42  31824  stoweidlem44  31826  stoweidlem45  31827  stoweidlem46  31828  stoweidlem47  31829  stoweidlem48  31830  stoweidlem50  31832  stoweidlem51  31833  stoweidlem52  31834  stoweidlem53  31835  stoweidlem54  31836  stoweidlem57  31839  stoweidlem59  31841  stoweidlem62  31844  wallispilem5  31851  stirlinglem4  31859  stirlinglem5  31860  stirlinglem8  31863  stirlinglem11  31866  stirlinglem12  31867  stirlinglem13  31868  stirlinglem14  31869  stirlinglem15  31870  fourierdlem20  31909  fourierdlem31  31920  fourierdlem68  31957  fourierdlem80  31969  fourierdlem89  31978  fourierdlem91  31980  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  fourierdlem115  32004  fourierd  32005  fourierclimd  32006  etransclem48  32065  nfafv  32221  nfaov  32264  bnj1230  33861  bnj1476  33905  bnj900  33987  bnj958  33998  bnj1000  33999  bnj1014  34018  bnj1123  34042  bnj1307  34079  bnj1321  34083  bnj1384  34088  bnj1398  34090  bnj1408  34092  bnj1444  34099  bnj1445  34100  bnj1446  34101  bnj1447  34102  bnj1448  34103  bnj1449  34104  bnj1466  34109  bnj1467  34110  bnj1518  34120  bnj1519  34121  bnj1520  34122  bnj1525  34125  bnj1523  34127  riotasv2s  34689  cdleme26ee  36086  cdlemefs32sn1aw  36140  cdleme43fsv1snlem  36146  cdleme41sn3a  36159  cdleme32d  36170  cdleme32f  36172  cdleme40m  36193  cdleme40n  36194  ltrniotaval  36307  cdlemksv2  36573  cdlemkuv2  36593  cdlemk36  36639  cdlemk38  36641  cdlemkid  36662  cdlemk19x  36669  cdlemk11t  36672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-nfc 2607
  Copyright terms: Public domain W3C validator