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

Theorem nfcxfr 2590
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  |-  A  =  B
nfcxfr.2  |-  F/_ x B
Assertion
Ref Expression
nfcxfr  |-  F/_ x A

Proof of Theorem nfcxfr
StepHypRef Expression
1 nfcxfr.2 . 2  |-  F/_ x B
2 nfceqi.1 . . 3  |-  A  =  B
32nfceqi 2589 . 2  |-  ( F/_ x A  <->  F/_ x B )
41, 3mpbir 213 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1444   F/_wnfc 2579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-12 1933  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-cleq 2444  df-clel 2447  df-nfc 2581
This theorem is referenced by:  nfrab1  2971  nfrab  2972  nfdif  3554  nfun  3590  nfin  3639  nfsymdif  3667  nfpw  3963  nfpr  4019  nfsn  4029  nfop  4182  nfuni  4204  nfint  4244  nfiun  4306  nfiin  4307  nfiu1  4308  nfii1  4309  nfopab  4468  nfopab1  4469  nfopab2  4470  nfmpt  4491  nfmpt1  4492  nfxp  4861  nfco  5000  nfcnv  5013  nfdm  5076  nfrn  5077  nfres  5107  nfima  5176  nfpred  5385  nfsuc  5494  nfiota1  5548  nffv  5872  fvmptss  5958  fvmptf  5966  fvopab5  5974  ralrnmpt  6031  f1ompt  6044  f1mpt  6162  fliftfun  6205  nfriota1  6259  riotaprop  6275  nfoprab1  6340  nfoprab2  6341  nfoprab3  6342  nfoprab  6343  nfmpt21  6358  nfmpt22  6359  nfmpt2  6360  ovmpt2s  6420  ov2gf  6421  ov3  6433  nftpos  7008  fvmpt2curryd  7018  nfwrecs  7030  nfrecs  7093  nfrdg  7132  rdgsucmptf  7146  rdgsucmptnf  7147  frsucmpt  7155  frsucmptn  7156  nfixp  7541  nfixp1  7542  xpcomco  7662  nfsup  7965  nfinf  7998  nfoi  8029  cnfcom3clem  8210  dfac8clem  8463  iunfo  8964  pwfseqlem2  9084  pwfseqlem4a  9086  pwfseqlem4  9087  reclem2pr  9473  nfseq  12223  nfwrd  12695  nfsum1  13756  nfsum  13757  nfcprod1  13964  nfcprod  13965  ptbasfi  20596  mbfsup  22620  itg1climres  22672  itg2splitlem  22706  itg2split  22707  nfitg1  22731  nfitg  22732  lgamgulm2  23961  lgseisenlem2  24278  cnlnadjlem5  27724  nfesum1  28861  nfesum2  28862  ballotlem7  29368  ballotlem7OLD  29406  bnj1230  29614  bnj1476  29658  bnj900  29740  bnj958  29751  bnj1000  29752  bnj1014  29771  bnj1123  29795  bnj1307  29832  bnj1321  29836  bnj1384  29841  bnj1398  29843  bnj1408  29845  bnj1444  29852  bnj1445  29853  bnj1446  29854  bnj1447  29855  bnj1448  29856  bnj1449  29857  bnj1466  29862  bnj1467  29863  bnj1518  29873  bnj1519  29874  bnj1520  29875  bnj1525  29878  bnj1523  29880  cvmcov  29986  nfwsuc  30501  nfwlim  30505  nfaltop  30747  topdifinfindis  31749  finxpreclem6  31788  sdclem1  32072  riotasv2s  32530  cdleme26ee  33927  cdlemefs32sn1aw  33981  cdleme43fsv1snlem  33987  cdleme41sn3a  34000  cdleme32d  34011  cdleme32f  34013  cdleme40m  34034  cdleme40n  34035  ltrniotaval  34148  cdlemksv2  34414  cdlemkuv2  34434  cdlemk36  34480  cdlemk38  34482  cdlemkid  34503  cdlemk19x  34510  cdlemk11t  34513  areaquad  36101  binomcxplemdvbinom  36702  binomcxplemdvsum  36704  binomcxplemnotnn0  36705  refsum2cnlem1  37358  suprnmpt  37439  wessf1ornlem  37459  disjrnmpt2  37463  fompt  37467  fmuldfeqlem1  37660  fmuldfeq  37661  mullimc  37696  idlimc  37706  limcperiod  37708  neglimc  37728  addlimc  37729  0ellimcdiv  37730  cncfmptssg  37747  cncfshift  37751  cncficcgt0  37766  cncfiooicclem1  37771  dvnmul  37818  dvnprodlem1  37821  itgsinexplem1  37830  itgsubsticclem  37852  stoweidlem14  37874  stoweidlem16  37876  stoweidlem18  37878  stoweidlem22  37882  stoweidlem26  37886  stoweidlem27  37887  stoweidlem31  37892  stoweidlem32  37893  stoweidlem34  37895  stoweidlem35  37896  stoweidlem40  37901  stoweidlem41  37902  stoweidlem42  37903  stoweidlem44  37905  stoweidlem45  37906  stoweidlem46  37907  stoweidlem47  37908  stoweidlem48  37909  stoweidlem50  37911  stoweidlem51  37912  stoweidlem52  37913  stoweidlem53  37914  stoweidlem54  37915  stoweidlem57  37918  stoweidlem59  37920  stoweidlem62  37923  stoweidlem62OLD  37924  wallispilem5  37931  stirlinglem4  37939  stirlinglem5  37940  stirlinglem8  37943  stirlinglem11  37946  stirlinglem12  37947  stirlinglem13  37948  stirlinglem14  37949  stirlinglem15  37950  fourierdlem20  37989  fourierdlem31  38000  fourierdlem31OLD  38001  fourierdlem68  38038  fourierdlem80  38050  fourierdlem89  38059  fourierdlem91  38061  fourierdlem103  38073  fourierdlem104  38074  fourierdlem112  38082  fourierdlem115  38085  fourierd  38086  fourierclimd  38087  etransclem48OLD  38147  etransclem48  38148  iundjiun  38298  ovnlerp  38384  ovncvrrp  38386  ovnhoilem1  38423  opnvonmbllem1  38454  nfafv  38638  nfaov  38681
  Copyright terms: Public domain W3C validator