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

Theorem nfcxfr 2569
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 2568 . 2  |-  ( F/_ x A  <->  F/_ x B )
41, 3mpbir 201 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    = wceq 1652   F/_wnfc 2559
This theorem is referenced by:  nfrab1  2888  nfrab  2889  nfdif  3468  nfun  3503  nfin  3547  nfpw  3810  nfpr  3855  nfsn  3866  nfop  4000  nfuni  4021  nfint  4060  nfiun  4119  nfiin  4120  nfiu1  4121  nfii1  4122  nfopab  4273  nfopab1  4274  nfopab2  4275  nfmpt  4297  nfmpt1  4298  nfsuc  4652  nfxp  4904  nfco  5038  nfcnv  5051  nfdm  5111  nfrn  5112  nfres  5148  nfima  5211  nfiota1  5420  nffv  5735  fvmptss  5813  fvmptf  5821  ralrnmpt  5878  f1ompt  5891  f1mpt  6007  fliftfun  6034  nfoprab1  6123  nfoprab2  6124  nfoprab3  6125  nfoprab  6126  nfmpt21  6140  nfmpt22  6141  nfmpt2  6142  ovmpt2s  6197  ov2gf  6198  ov3  6210  nftpos  6514  fvopab5  6534  nfriota1  6557  riotaprop  6573  riotasv2s  6596  nfrecs  6635  nfrdg  6672  rdgsucmptf  6686  rdgsucmptnf  6687  frsucmpt  6695  frsucmptn  6696  nfixp  7081  nfixp1  7082  xpcomco  7198  nfsup  7456  nfoi  7483  cnfcom3clem  7662  dfac8clem  7913  iunfo  8414  pwfseqlem2  8534  pwfseqlem4a  8536  pwfseqlem4  8537  reclem2pr  8925  nfseq  11333  nfwrd  11740  nfsum1  12484  nfsum  12485  ptbasfi  17613  mbfsup  19556  itg1climres  19606  itg2splitlem  19640  itg2split  19641  nfitg1  19665  nfitg  19666  lgseisenlem2  21134  cnlnadjlem5  23574  nfesum1  24437  ballotlem7  24793  lgamgulm2  24820  cvmcov  24950  nfcprod1  25236  nfcprod  25237  nfpred  25444  nfwrecs  25533  nfwsuc  25569  nfwlim  25573  nfsymdif  25667  nfaltop  25825  sdclem1  26447  refsum2cnlem1  27684  fmuldfeqlem1  27688  fmuldfeq  27689  itgsinexplem1  27724  stoweidlem14  27739  stoweidlem16  27741  stoweidlem18  27743  stoweidlem22  27747  stoweidlem26  27751  stoweidlem27  27752  stoweidlem31  27756  stoweidlem32  27757  stoweidlem34  27759  stoweidlem35  27760  stoweidlem40  27765  stoweidlem41  27766  stoweidlem42  27767  stoweidlem44  27769  stoweidlem45  27770  stoweidlem46  27771  stoweidlem47  27772  stoweidlem48  27773  stoweidlem50  27775  stoweidlem51  27776  stoweidlem52  27777  stoweidlem53  27778  stoweidlem54  27779  stoweidlem57  27782  stoweidlem59  27784  stoweidlem62  27787  wallispilem5  27794  stirlinglem4  27802  stirlinglem5  27803  stirlinglem8  27806  stirlinglem11  27809  stirlinglem12  27810  stirlinglem13  27811  stirlinglem14  27812  stirlinglem15  27813  nfafv  27976  nfaov  28019  bnj1230  29174  bnj1476  29218  bnj900  29300  bnj958  29311  bnj1000  29312  bnj1014  29331  bnj1123  29355  bnj1307  29392  bnj1321  29396  bnj1384  29401  bnj1398  29403  bnj1408  29405  bnj1444  29412  bnj1445  29413  bnj1446  29414  bnj1447  29415  bnj1448  29416  bnj1449  29417  bnj1466  29422  bnj1467  29423  bnj1518  29433  bnj1519  29434  bnj1520  29435  bnj1525  29438  bnj1523  29440  cdleme26ee  31157  cdlemefs32sn1aw  31211  cdleme43fsv1snlem  31217  cdleme41sn3a  31230  cdleme32d  31241  cdleme32f  31243  cdleme40m  31264  cdleme40n  31265  ltrniotaval  31378  cdlemksv2  31644  cdlemkuv2  31664  cdlemk36  31710  cdlemk38  31712  cdlemkid  31733  cdlemk19x  31740  cdlemk11t  31743
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-cleq 2429  df-clel 2432  df-nfc 2561
  Copyright terms: Public domain W3C validator