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

Theorem nfcxfr 2614
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 2612 . 2  |-  ( F/_ x A  <->  F/_ x B )
41, 3mpbir 209 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398   F/_wnfc 2602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-12 1859  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-cleq 2446  df-clel 2449  df-nfc 2604
This theorem is referenced by:  nfrab1  3035  nfrab  3036  nfdif  3611  nfun  3646  nfin  3691  nfsymdif  3719  nfpw  4011  nfpr  4063  nfsn  4073  nfop  4219  nfuni  4241  nfint  4281  nfiun  4343  nfiin  4344  nfiu1  4345  nfii1  4346  nfopab  4504  nfopab1  4505  nfopab2  4506  nfmpt  4527  nfmpt1  4528  nfsuc  4938  nfxp  5015  nfco  5157  nfcnv  5170  nfdm  5233  nfrn  5234  nfres  5264  nfima  5333  nfiota1  5536  nffv  5855  fvmptss  5940  fvmptf  5948  fvopab5  5955  ralrnmpt  6016  f1ompt  6029  f1mpt  6144  fliftfun  6185  nfriota1  6239  riotaprop  6255  nfoprab1  6319  nfoprab2  6320  nfoprab3  6321  nfoprab  6322  nfmpt21  6337  nfmpt22  6338  nfmpt2  6339  ovmpt2s  6399  ov2gf  6400  ov3  6412  nftpos  6982  fvmpt2curryd  6992  nfrecs  7036  nfrdg  7072  rdgsucmptf  7086  rdgsucmptnf  7087  frsucmpt  7095  frsucmptn  7096  nfixp  7481  nfixp1  7482  xpcomco  7600  nfsup  7902  nfoi  7931  cnfcom3clem  8140  cnfcom3clemOLD  8148  dfac8clem  8404  iunfo  8905  pwfseqlem2  9026  pwfseqlem4a  9028  pwfseqlem4  9029  reclem2pr  9415  nfseq  12099  nfwrd  12557  nfsum1  13594  nfsum  13595  nfcprod1  13799  nfcprod  13800  ptbasfi  20248  mbfsup  22237  itg1climres  22287  itg2splitlem  22321  itg2split  22322  nfitg1  22346  nfitg  22347  lgseisenlem2  23823  cnlnadjlem5  27188  nfesum1  28269  nfesum2  28270  ballotlem7  28738  lgamgulm2  28842  cvmcov  28972  nfpred  29489  nfwrecs  29578  nfwsuc  29614  nfwlim  29618  nfaltop  29858  sdclem1  30476  areaquad  31425  binomcxplemdvbinom  31499  binomcxplemdvsum  31501  binomcxplemnotnn0  31502  refsum2cnlem1  31652  suprnmpt  31691  fmuldfeqlem1  31815  fmuldfeq  31816  mullimc  31861  idlimc  31871  limcperiod  31873  neglimc  31892  addlimc  31893  0ellimcdiv  31894  cncfmptssg  31911  cncfshift  31915  cncficcgt0  31930  cncfiooicclem1  31935  dvnmul  31979  dvnprodlem1  31982  itgsinexplem1  31991  itgsubsticclem  32013  stoweidlem14  32035  stoweidlem16  32037  stoweidlem18  32039  stoweidlem22  32043  stoweidlem26  32047  stoweidlem27  32048  stoweidlem31  32052  stoweidlem32  32053  stoweidlem34  32055  stoweidlem35  32056  stoweidlem40  32061  stoweidlem41  32062  stoweidlem42  32063  stoweidlem44  32065  stoweidlem45  32066  stoweidlem46  32067  stoweidlem47  32068  stoweidlem48  32069  stoweidlem50  32071  stoweidlem51  32072  stoweidlem52  32073  stoweidlem53  32074  stoweidlem54  32075  stoweidlem57  32078  stoweidlem59  32080  stoweidlem62  32083  wallispilem5  32090  stirlinglem4  32098  stirlinglem5  32099  stirlinglem8  32102  stirlinglem11  32105  stirlinglem12  32106  stirlinglem13  32107  stirlinglem14  32108  stirlinglem15  32109  fourierdlem20  32148  fourierdlem31  32159  fourierdlem68  32196  fourierdlem80  32208  fourierdlem89  32217  fourierdlem91  32219  fourierdlem103  32231  fourierdlem104  32232  fourierdlem112  32240  fourierdlem115  32243  fourierd  32244  fourierclimd  32245  etransclem48  32304  nfafv  32460  nfaov  32503  bnj1230  34262  bnj1476  34306  bnj900  34388  bnj958  34399  bnj1000  34400  bnj1014  34419  bnj1123  34443  bnj1307  34480  bnj1321  34484  bnj1384  34489  bnj1398  34491  bnj1408  34493  bnj1444  34500  bnj1445  34501  bnj1446  34502  bnj1447  34503  bnj1448  34504  bnj1449  34505  bnj1466  34510  bnj1467  34511  bnj1518  34521  bnj1519  34522  bnj1520  34523  bnj1525  34526  bnj1523  34528  riotasv2s  35086  cdleme26ee  36483  cdlemefs32sn1aw  36537  cdleme43fsv1snlem  36543  cdleme41sn3a  36556  cdleme32d  36567  cdleme32f  36569  cdleme40m  36590  cdleme40n  36591  ltrniotaval  36704  cdlemksv2  36970  cdlemkuv2  36990  cdlemk36  37036  cdlemk38  37038  cdlemkid  37059  cdlemk19x  37066  cdlemk11t  37069
  Copyright terms: Public domain W3C validator