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

Theorem nfcxfr 2574
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 2573 . 2  |-  ( F/_ x A  <->  F/_ x B )
41, 3mpbir 209 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1364   F/_wnfc 2564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-cleq 2434  df-clel 2437  df-nfc 2566
This theorem is referenced by:  nfrab1  2899  nfrab  2900  nfdif  3474  nfun  3509  nfin  3554  nfpw  3869  nfpr  3920  nfsn  3931  nfop  4072  nfuni  4094  nfint  4135  nfiun  4195  nfiin  4196  nfiu1  4197  nfii1  4198  nfopab  4354  nfopab1  4355  nfopab2  4356  nfmpt  4377  nfmpt1  4378  nfsuc  4786  nfxp  4862  nfco  5001  nfcnv  5014  nfdm  5077  nfrn  5078  nfres  5108  nfima  5174  nfiota1  5380  nffv  5695  fvmptss  5779  fvmptf  5787  fvopab5  5792  ralrnmpt  5849  f1ompt  5862  f1mpt  5971  fliftfun  6002  nfriota1  6057  riotaprop  6074  nfoprab1  6134  nfoprab2  6135  nfoprab3  6136  nfoprab  6137  nfmpt21  6152  nfmpt22  6153  nfmpt2  6154  ovmpt2s  6213  ov2gf  6214  ov3  6226  nftpos  6779  nfrecs  6830  nfrdg  6866  rdgsucmptf  6880  rdgsucmptnf  6881  frsucmpt  6889  frsucmptn  6890  nfixp  7278  nfixp1  7279  xpcomco  7397  nfsup  7697  nfoi  7724  cnfcom3clem  7934  cnfcom3clemOLD  7942  dfac8clem  8198  iunfo  8699  pwfseqlem2  8822  pwfseqlem4a  8824  pwfseqlem4  8825  reclem2pr  9213  nfseq  11812  nfwrd  12252  nfsum1  13163  nfsum  13164  ptbasfi  19113  mbfsup  21101  itg1climres  21151  itg2splitlem  21185  itg2split  21186  nfitg1  21210  nfitg  21211  lgseisenlem2  22648  cnlnadjlem5  25410  nfesum1  26432  ballotlem7  26848  lgamgulm2  26952  cvmcov  27082  nfcprod1  27352  nfcprod  27353  nfpred  27559  nfwrecs  27648  nfwsuc  27684  nfwlim  27688  nfsymdif  27782  nfaltop  27940  sdclem1  28564  areaquad  29517  refsum2cnlem1  29684  fmuldfeqlem1  29688  fmuldfeq  29689  itgsinexplem1  29719  stoweidlem14  29734  stoweidlem16  29736  stoweidlem18  29738  stoweidlem22  29742  stoweidlem26  29746  stoweidlem27  29747  stoweidlem31  29751  stoweidlem32  29752  stoweidlem34  29754  stoweidlem35  29755  stoweidlem40  29760  stoweidlem41  29761  stoweidlem42  29762  stoweidlem44  29764  stoweidlem45  29765  stoweidlem46  29766  stoweidlem47  29767  stoweidlem48  29768  stoweidlem50  29770  stoweidlem51  29771  stoweidlem52  29772  stoweidlem53  29773  stoweidlem54  29774  stoweidlem57  29777  stoweidlem59  29779  stoweidlem62  29782  wallispilem5  29789  stirlinglem4  29797  stirlinglem5  29798  stirlinglem8  29801  stirlinglem11  29804  stirlinglem12  29805  stirlinglem13  29806  stirlinglem14  29807  stirlinglem15  29808  nfafv  29967  nfaov  30010  bnj1230  31630  bnj1476  31674  bnj900  31756  bnj958  31767  bnj1000  31768  bnj1014  31787  bnj1123  31811  bnj1307  31848  bnj1321  31852  bnj1384  31857  bnj1398  31859  bnj1408  31861  bnj1444  31868  bnj1445  31869  bnj1446  31870  bnj1447  31871  bnj1448  31872  bnj1449  31873  bnj1466  31878  bnj1467  31879  bnj1518  31889  bnj1519  31890  bnj1520  31891  bnj1525  31894  bnj1523  31896  riotasv2s  32331  cdleme26ee  33726  cdlemefs32sn1aw  33780  cdleme43fsv1snlem  33786  cdleme41sn3a  33799  cdleme32d  33810  cdleme32f  33812  cdleme40m  33833  cdleme40n  33834  ltrniotaval  33947  cdlemksv2  34213  cdlemkuv2  34233  cdlemk36  34279  cdlemk38  34281  cdlemkid  34302  cdlemk19x  34309  cdlemk11t  34312
  Copyright terms: Public domain W3C validator