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

Theorem nfcxfr 2610
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 2609 . 2  |-  ( F/_ x A  <->  F/_ x B )
41, 3mpbir 214 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1452   F/_wnfc 2599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-cleq 2464  df-clel 2467  df-nfc 2601
This theorem is referenced by:  nfrab1  2957  nfrab  2958  nfdif  3543  nfun  3581  nfin  3630  nfsymdif  3658  nfpw  3954  nfpr  4010  nfsn  4020  nfop  4174  nfuni  4196  nfint  4236  nfiun  4297  nfiin  4298  nfiu1  4299  nfii1  4300  nfopab  4461  nfopab1  4462  nfopab2  4463  nfmpt  4484  nfmpt1  4485  nfxp  4866  nfco  5005  nfcnv  5018  nfdm  5082  nfrn  5083  nfres  5113  nfima  5182  nfpred  5392  nfsuc  5501  nfiota1  5555  nffv  5886  fvmptss  5973  fvmptf  5981  fvopab5  5989  ralrnmpt  6046  f1ompt  6059  f1mpt  6180  fliftfun  6223  nfriota1  6277  riotaprop  6293  nfoprab1  6359  nfoprab2  6360  nfoprab3  6361  nfoprab  6362  nfmpt21  6377  nfmpt22  6378  nfmpt2  6379  ovmpt2s  6439  ov2gf  6440  ov3  6452  nftpos  7026  fvmpt2curryd  7036  nfwrecs  7048  nfrecs  7111  nfrdg  7150  rdgsucmptf  7164  rdgsucmptnf  7165  frsucmpt  7173  frsucmptn  7174  nfixp  7559  nfixp1  7560  xpcomco  7680  nfsup  7983  nfinf  8016  nfoi  8047  cnfcom3clem  8228  dfac8clem  8481  iunfo  8982  pwfseqlem2  9102  pwfseqlem4a  9104  pwfseqlem4  9105  reclem2pr  9491  nfseq  12261  nfwrd  12746  nfsum1  13833  nfsum  13834  nfcprod1  14041  nfcprod  14042  ptbasfi  20673  mbfsup  22699  itg1climres  22751  itg2splitlem  22785  itg2split  22786  nfitg1  22810  nfitg  22811  lgamgulm2  24040  lgseisenlem2  24357  cnlnadjlem5  27805  nfesum1  28935  nfesum2  28936  ballotlem7  29441  ballotlem7OLD  29479  bnj1230  29686  bnj1476  29730  bnj900  29812  bnj958  29823  bnj1000  29824  bnj1014  29843  bnj1123  29867  bnj1307  29904  bnj1321  29908  bnj1384  29913  bnj1398  29915  bnj1408  29917  bnj1444  29924  bnj1445  29925  bnj1446  29926  bnj1447  29927  bnj1448  29928  bnj1449  29929  bnj1466  29934  bnj1467  29935  bnj1518  29945  bnj1519  29946  bnj1520  29947  bnj1525  29950  bnj1523  29952  cvmcov  30058  nfwsuc  30572  nfwlim  30576  nfaltop  30818  topdifinfindis  31819  finxpreclem6  31858  sdclem1  32136  riotasv2s  32594  cdleme26ee  33998  cdlemefs32sn1aw  34052  cdleme43fsv1snlem  34058  cdleme41sn3a  34071  cdleme32d  34082  cdleme32f  34084  cdleme40m  34105  cdleme40n  34106  ltrniotaval  34219  cdlemksv2  34485  cdlemkuv2  34505  cdlemk36  34551  cdlemk38  34553  cdlemkid  34574  cdlemk19x  34581  cdlemk11t  34584  areaquad  36172  binomcxplemdvbinom  36772  binomcxplemdvsum  36774  binomcxplemnotnn0  36775  refsum2cnlem1  37421  suprnmpt  37512  wessf1ornlem  37530  disjrnmpt2  37534  fompt  37538  fmuldfeqlem1  37757  fmuldfeq  37758  mullimc  37793  idlimc  37803  limcperiod  37805  neglimc  37825  addlimc  37826  0ellimcdiv  37827  cncfmptssg  37844  cncfshift  37848  cncficcgt0  37863  cncfiooicclem1  37868  dvnmul  37915  dvnprodlem1  37918  itgsinexplem1  37927  itgsubsticclem  37949  stoweidlem14  37986  stoweidlem16  37988  stoweidlem18  37990  stoweidlem22  37994  stoweidlem26  37998  stoweidlem27  37999  stoweidlem31  38004  stoweidlem32  38005  stoweidlem34  38007  stoweidlem35  38008  stoweidlem40  38013  stoweidlem41  38014  stoweidlem42  38015  stoweidlem44  38017  stoweidlem45  38018  stoweidlem46  38019  stoweidlem47  38020  stoweidlem48  38021  stoweidlem50  38023  stoweidlem51  38024  stoweidlem52  38025  stoweidlem53  38026  stoweidlem54  38027  stoweidlem57  38030  stoweidlem59  38032  stoweidlem62  38035  stoweidlem62OLD  38036  wallispilem5  38043  stirlinglem4  38051  stirlinglem5  38052  stirlinglem8  38055  stirlinglem11  38058  stirlinglem12  38059  stirlinglem13  38060  stirlinglem14  38061  stirlinglem15  38062  fourierdlem20  38101  fourierdlem31  38112  fourierdlem31OLD  38113  fourierdlem68  38150  fourierdlem80  38162  fourierdlem89  38171  fourierdlem91  38173  fourierdlem103  38185  fourierdlem104  38186  fourierdlem112  38194  fourierdlem115  38197  fourierd  38198  fourierclimd  38199  etransclem48OLD  38259  etransclem48  38260  iundjiun  38414  ovnlerp  38502  ovncvrrp  38504  ovnhoilem1  38541  opnvonmbllem1  38572  nfafv  38783  nfaov  38826  lfgrnloop  39370
  Copyright terms: Public domain W3C validator