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

Theorem nfcxfr 2580
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 2578 . 2  |-  ( F/_ x A  <->  F/_ x B )
41, 3mpbir 212 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   F/_wnfc 2568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-12 1904  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-cleq 2412  df-clel 2415  df-nfc 2570
This theorem is referenced by:  nfrab1  3007  nfrab  3008  nfdif  3583  nfun  3619  nfin  3666  nfsymdif  3694  nfpw  3988  nfpr  4041  nfsn  4051  nfop  4197  nfuni  4219  nfint  4259  nfiun  4321  nfiin  4322  nfiu1  4323  nfii1  4324  nfopab  4482  nfopab1  4483  nfopab2  4484  nfmpt  4505  nfmpt1  4506  nfxp  4872  nfco  5011  nfcnv  5024  nfdm  5087  nfrn  5088  nfres  5118  nfima  5187  nfpred  5395  nfsuc  5504  nfiota1  5558  nffv  5879  fvmptss  5965  fvmptf  5973  fvopab5  5980  ralrnmpt  6037  f1ompt  6050  f1mpt  6168  fliftfun  6211  nfriota1  6265  riotaprop  6281  nfoprab1  6345  nfoprab2  6346  nfoprab3  6347  nfoprab  6348  nfmpt21  6363  nfmpt22  6364  nfmpt2  6365  ovmpt2s  6425  ov2gf  6426  ov3  6438  nftpos  7007  fvmpt2curryd  7017  nfwrecs  7029  nfrecs  7092  nfrdg  7131  rdgsucmptf  7145  rdgsucmptnf  7146  frsucmpt  7154  frsucmptn  7155  nfixp  7540  nfixp1  7541  xpcomco  7659  nfsup  7962  nfinf  7995  nfoi  8020  cnfcom3clem  8200  dfac8clem  8452  iunfo  8953  pwfseqlem2  9073  pwfseqlem4a  9075  pwfseqlem4  9076  reclem2pr  9462  nfseq  12209  nfwrd  12671  nfsum1  13723  nfsum  13724  nfcprod1  13931  nfcprod  13932  ptbasfi  20520  mbfsup  22494  itg1climres  22546  itg2splitlem  22580  itg2split  22581  nfitg1  22605  nfitg  22606  lgamgulm2  23823  lgseisenlem2  24138  cnlnadjlem5  27556  nfesum1  28697  nfesum2  28698  ballotlem7  29191  bnj1230  29399  bnj1476  29443  bnj900  29525  bnj958  29536  bnj1000  29537  bnj1014  29556  bnj1123  29580  bnj1307  29617  bnj1321  29621  bnj1384  29626  bnj1398  29628  bnj1408  29630  bnj1444  29637  bnj1445  29638  bnj1446  29639  bnj1447  29640  bnj1448  29641  bnj1449  29642  bnj1466  29647  bnj1467  29648  bnj1518  29658  bnj1519  29659  bnj1520  29660  bnj1525  29663  bnj1523  29665  cvmcov  29771  nfwsuc  30285  nfwlim  30289  nfaltop  30529  topdifinfindis  31480  sdclem1  31776  riotasv2s  32239  cdleme26ee  33636  cdlemefs32sn1aw  33690  cdleme43fsv1snlem  33696  cdleme41sn3a  33709  cdleme32d  33720  cdleme32f  33722  cdleme40m  33743  cdleme40n  33744  ltrniotaval  33857  cdlemksv2  34123  cdlemkuv2  34143  cdlemk36  34189  cdlemk38  34191  cdlemkid  34212  cdlemk19x  34219  cdlemk11t  34222  areaquad  35804  binomcxplemdvbinom  36343  binomcxplemdvsum  36345  binomcxplemnotnn0  36346  refsum2cnlem1  37002  suprnmpt  37065  wessf1ornlem  37086  disjrnmpt2  37090  fompt  37094  fmuldfeqlem1  37236  fmuldfeq  37237  mullimc  37272  idlimc  37282  limcperiod  37284  neglimc  37304  addlimc  37305  0ellimcdiv  37306  cncfmptssg  37323  cncfshift  37327  cncficcgt0  37342  cncfiooicclem1  37347  dvnmul  37391  dvnprodlem1  37394  itgsinexplem1  37403  itgsubsticclem  37425  stoweidlem14  37447  stoweidlem16  37449  stoweidlem18  37451  stoweidlem22  37455  stoweidlem26  37459  stoweidlem27  37460  stoweidlem31  37465  stoweidlem32  37466  stoweidlem34  37468  stoweidlem35  37469  stoweidlem40  37474  stoweidlem41  37475  stoweidlem42  37476  stoweidlem44  37478  stoweidlem45  37479  stoweidlem46  37480  stoweidlem47  37481  stoweidlem48  37482  stoweidlem50  37484  stoweidlem51  37485  stoweidlem52  37486  stoweidlem53  37487  stoweidlem54  37488  stoweidlem57  37491  stoweidlem59  37493  stoweidlem62  37496  stoweidlem62OLD  37497  wallispilem5  37504  stirlinglem4  37512  stirlinglem5  37513  stirlinglem8  37516  stirlinglem11  37519  stirlinglem12  37520  stirlinglem13  37521  stirlinglem14  37522  stirlinglem15  37523  fourierdlem20  37562  fourierdlem31  37573  fourierdlem68  37610  fourierdlem80  37622  fourierdlem89  37631  fourierdlem91  37633  fourierdlem103  37645  fourierdlem104  37646  fourierdlem112  37654  fourierdlem115  37657  fourierd  37658  fourierclimd  37659  etransclem48  37718  iundjiun  37811  nfafv  38041  nfaov  38084
  Copyright terms: Public domain W3C validator