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

Theorem nfcxfr 2587
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 2585 . 2  |-  ( F/_ x A  <->  F/_ x B )
41, 3mpbir 209 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369   F/_wnfc 2575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-cleq 2436  df-clel 2439  df-nfc 2577
This theorem is referenced by:  nfrab1  2913  nfrab  2914  nfdif  3489  nfun  3524  nfin  3569  nfpw  3884  nfpr  3935  nfsn  3946  nfop  4087  nfuni  4109  nfint  4150  nfiun  4210  nfiin  4211  nfiu1  4212  nfii1  4213  nfopab  4369  nfopab1  4370  nfopab2  4371  nfmpt  4392  nfmpt1  4393  nfsuc  4802  nfxp  4878  nfco  5017  nfcnv  5030  nfdm  5093  nfrn  5094  nfres  5124  nfima  5189  nfiota1  5395  nffv  5710  fvmptss  5794  fvmptf  5802  fvopab5  5807  ralrnmpt  5864  f1ompt  5877  f1mpt  5986  fliftfun  6017  nfriota1  6071  riotaprop  6088  nfoprab1  6147  nfoprab2  6148  nfoprab3  6149  nfoprab  6150  nfmpt21  6165  nfmpt22  6166  nfmpt2  6167  ovmpt2s  6226  ov2gf  6227  ov3  6239  nftpos  6792  fvmpt2curryd  6802  nfrecs  6846  nfrdg  6882  rdgsucmptf  6896  rdgsucmptnf  6897  frsucmpt  6905  frsucmptn  6906  nfixp  7294  nfixp1  7295  xpcomco  7413  nfsup  7713  nfoi  7740  cnfcom3clem  7950  cnfcom3clemOLD  7958  dfac8clem  8214  iunfo  8715  pwfseqlem2  8838  pwfseqlem4a  8840  pwfseqlem4  8841  reclem2pr  9229  nfseq  11828  nfwrd  12268  nfsum1  13179  nfsum  13180  ptbasfi  19166  mbfsup  21154  itg1climres  21204  itg2splitlem  21238  itg2split  21239  nfitg1  21263  nfitg  21264  lgseisenlem2  22701  cnlnadjlem5  25487  nfesum1  26508  ballotlem7  26930  lgamgulm2  27034  cvmcov  27164  nfcprod1  27435  nfcprod  27436  nfpred  27642  nfwrecs  27731  nfwsuc  27767  nfwlim  27771  nfsymdif  27865  nfaltop  28023  sdclem1  28651  areaquad  29604  refsum2cnlem1  29771  fmuldfeqlem1  29775  fmuldfeq  29776  itgsinexplem1  29806  stoweidlem14  29821  stoweidlem16  29823  stoweidlem18  29825  stoweidlem22  29829  stoweidlem26  29833  stoweidlem27  29834  stoweidlem31  29838  stoweidlem32  29839  stoweidlem34  29841  stoweidlem35  29842  stoweidlem40  29847  stoweidlem41  29848  stoweidlem42  29849  stoweidlem44  29851  stoweidlem45  29852  stoweidlem46  29853  stoweidlem47  29854  stoweidlem48  29855  stoweidlem50  29857  stoweidlem51  29858  stoweidlem52  29859  stoweidlem53  29860  stoweidlem54  29861  stoweidlem57  29864  stoweidlem59  29866  stoweidlem62  29869  wallispilem5  29876  stirlinglem4  29884  stirlinglem5  29885  stirlinglem8  29888  stirlinglem11  29891  stirlinglem12  29892  stirlinglem13  29893  stirlinglem14  29894  stirlinglem15  29895  nfafv  30054  nfaov  30097  bnj1230  31808  bnj1476  31852  bnj900  31934  bnj958  31945  bnj1000  31946  bnj1014  31965  bnj1123  31989  bnj1307  32026  bnj1321  32030  bnj1384  32035  bnj1398  32037  bnj1408  32039  bnj1444  32046  bnj1445  32047  bnj1446  32048  bnj1447  32049  bnj1448  32050  bnj1449  32051  bnj1466  32056  bnj1467  32057  bnj1518  32067  bnj1519  32068  bnj1520  32069  bnj1525  32072  bnj1523  32074  riotasv2s  32621  cdleme26ee  34016  cdlemefs32sn1aw  34070  cdleme43fsv1snlem  34076  cdleme41sn3a  34089  cdleme32d  34100  cdleme32f  34102  cdleme40m  34123  cdleme40n  34124  ltrniotaval  34237  cdlemksv2  34503  cdlemkuv2  34523  cdlemk36  34569  cdlemk38  34571  cdlemkid  34592  cdlemk19x  34599  cdlemk11t  34602
  Copyright terms: Public domain W3C validator