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

Theorem nfcxfr 2627
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 2625 . 2  |-  ( F/_ x A  <->  F/_ x B )
41, 3mpbir 209 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379   F/_wnfc 2615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-clel 2462  df-nfc 2617
This theorem is referenced by:  nfrab1  3042  nfrab  3043  nfdif  3625  nfun  3660  nfin  3705  nfpw  4022  nfpr  4074  nfsn  4085  nfop  4229  nfuni  4251  nfint  4292  nfiun  4353  nfiin  4354  nfiu1  4355  nfii1  4356  nfopab  4512  nfopab1  4513  nfopab2  4514  nfmpt  4535  nfmpt1  4536  nfsuc  4949  nfxp  5025  nfco  5167  nfcnv  5180  nfdm  5243  nfrn  5244  nfres  5274  nfima  5344  nfiota1  5552  nffv  5872  fvmptss  5957  fvmptf  5965  fvopab5  5972  ralrnmpt  6029  f1ompt  6042  f1mpt  6156  fliftfun  6197  nfriota1  6251  riotaprop  6268  nfoprab1  6329  nfoprab2  6330  nfoprab3  6331  nfoprab  6332  nfmpt21  6347  nfmpt22  6348  nfmpt2  6349  ovmpt2s  6409  ov2gf  6410  ov3  6422  nftpos  6990  fvmpt2curryd  7000  nfrecs  7044  nfrdg  7080  rdgsucmptf  7094  rdgsucmptnf  7095  frsucmpt  7103  frsucmptn  7104  nfixp  7488  nfixp1  7489  xpcomco  7607  nfsup  7910  nfoi  7938  cnfcom3clem  8148  cnfcom3clemOLD  8156  dfac8clem  8412  iunfo  8913  pwfseqlem2  9036  pwfseqlem4a  9038  pwfseqlem4  9039  reclem2pr  9425  nfseq  12084  nfwrd  12534  nfsum1  13474  nfsum  13475  ptbasfi  19833  mbfsup  21822  itg1climres  21872  itg2splitlem  21906  itg2split  21907  nfitg1  21931  nfitg  21932  lgseisenlem2  23369  cnlnadjlem5  26682  nfesum1  27709  ballotlem7  28130  lgamgulm2  28234  cvmcov  28364  nfcprod1  28635  nfcprod  28636  nfpred  28842  nfwrecs  28931  nfwsuc  28967  nfwlim  28971  nfsymdif  29065  nfaltop  29223  sdclem1  29855  areaquad  30805  refsum2cnlem1  31006  suprnmpt  31045  fmuldfeqlem1  31148  fmuldfeq  31149  mullimc  31174  idlimc  31184  limcperiod  31186  neglimc  31205  addlimc  31206  0ellimcdiv  31207  cncfmptssg  31224  cncfshift  31228  icccncfext  31242  cncficcgt0  31243  cncfiooicclem1  31248  itgsinexplem1  31287  itgsubsticclem  31309  stoweidlem14  31330  stoweidlem16  31332  stoweidlem18  31334  stoweidlem22  31338  stoweidlem26  31342  stoweidlem27  31343  stoweidlem31  31347  stoweidlem32  31348  stoweidlem34  31350  stoweidlem35  31351  stoweidlem40  31356  stoweidlem41  31357  stoweidlem42  31358  stoweidlem44  31360  stoweidlem45  31361  stoweidlem46  31362  stoweidlem47  31363  stoweidlem48  31364  stoweidlem50  31366  stoweidlem51  31367  stoweidlem52  31368  stoweidlem53  31369  stoweidlem54  31370  stoweidlem57  31373  stoweidlem59  31375  stoweidlem62  31378  wallispilem5  31385  stirlinglem4  31393  stirlinglem5  31394  stirlinglem8  31397  stirlinglem11  31400  stirlinglem12  31401  stirlinglem13  31402  stirlinglem14  31403  stirlinglem15  31404  fourierdlem20  31443  fourierdlem31  31454  fourierdlem68  31491  fourierdlem80  31503  fourierdlem89  31512  fourierdlem91  31514  fourierdlem103  31526  fourierdlem104  31527  fourierdlem112  31535  fourierdlem115  31538  fourierd  31539  fourierclimd  31540  nfafv  31704  nfaov  31747  bnj1230  32949  bnj1476  32993  bnj900  33075  bnj958  33086  bnj1000  33087  bnj1014  33106  bnj1123  33130  bnj1307  33167  bnj1321  33171  bnj1384  33176  bnj1398  33178  bnj1408  33180  bnj1444  33187  bnj1445  33188  bnj1446  33189  bnj1447  33190  bnj1448  33191  bnj1449  33192  bnj1466  33197  bnj1467  33198  bnj1518  33208  bnj1519  33209  bnj1520  33210  bnj1525  33213  bnj1523  33215  riotasv2s  33770  cdleme26ee  35165  cdlemefs32sn1aw  35219  cdleme43fsv1snlem  35225  cdleme41sn3a  35238  cdleme32d  35249  cdleme32f  35251  cdleme40m  35272  cdleme40n  35273  ltrniotaval  35386  cdlemksv2  35652  cdlemkuv2  35672  cdlemk36  35718  cdlemk38  35720  cdlemkid  35741  cdlemk19x  35748  cdlemk11t  35751
  Copyright terms: Public domain W3C validator