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

Theorem nfcxfr 2537
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 2536 . 2  |-  ( F/_ x A  <->  F/_ x B )
41, 3mpbir 201 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    = wceq 1649   F/_wnfc 2527
This theorem is referenced by:  nfrab1  2848  nfrab  2849  nfdif  3428  nfun  3463  nfin  3507  nfpw  3770  nfpr  3815  nfsn  3826  nfop  3960  nfuni  3981  nfint  4020  nfiun  4079  nfiin  4080  nfiu1  4081  nfii1  4082  nfopab  4233  nfopab1  4234  nfopab2  4235  nfmpt  4257  nfmpt1  4258  nfsuc  4612  nfxp  4863  nfco  4997  nfcnv  5010  nfdm  5070  nfrn  5071  nfres  5107  nfima  5170  nfiota1  5379  nffv  5694  fvmptss  5772  fvmptf  5780  ralrnmpt  5837  f1ompt  5850  f1mpt  5966  fliftfun  5993  nfoprab1  6082  nfoprab2  6083  nfoprab3  6084  nfoprab  6085  nfmpt21  6099  nfmpt22  6100  nfmpt2  6101  ovmpt2s  6156  ov2gf  6157  ov3  6169  nftpos  6473  fvopab5  6493  nfriota1  6516  riotaprop  6532  riotasv2s  6555  nfrecs  6594  nfrdg  6631  rdgsucmptf  6645  rdgsucmptnf  6646  frsucmpt  6654  frsucmptn  6655  nfixp  7040  nfixp1  7041  xpcomco  7157  nfsup  7412  nfoi  7439  cnfcom3clem  7618  dfac8clem  7869  iunfo  8370  pwfseqlem2  8490  pwfseqlem4a  8492  pwfseqlem4  8493  reclem2pr  8881  nfseq  11288  nfwrd  11695  nfsum1  12439  nfsum  12440  ptbasfi  17566  mbfsup  19509  itg1climres  19559  itg2splitlem  19593  itg2split  19594  nfitg1  19618  nfitg  19619  lgseisenlem2  21087  cnlnadjlem5  23527  nfesum1  24390  ballotlem7  24746  lgamgulm2  24773  cvmcov  24903  nfcprod1  25189  nfcprod  25190  nfsymdif  25580  nfaltop  25729  sdclem1  26337  refsum2cnlem1  27575  fmuldfeqlem1  27579  fmuldfeq  27580  itgsinexplem1  27615  stoweidlem14  27630  stoweidlem16  27632  stoweidlem18  27634  stoweidlem22  27638  stoweidlem26  27642  stoweidlem27  27643  stoweidlem31  27647  stoweidlem32  27648  stoweidlem34  27650  stoweidlem35  27651  stoweidlem40  27656  stoweidlem41  27657  stoweidlem42  27658  stoweidlem44  27660  stoweidlem45  27661  stoweidlem46  27662  stoweidlem47  27663  stoweidlem48  27664  stoweidlem50  27666  stoweidlem51  27667  stoweidlem52  27668  stoweidlem53  27669  stoweidlem54  27670  stoweidlem57  27673  stoweidlem59  27675  stoweidlem62  27678  wallispilem5  27685  stirlinglem4  27693  stirlinglem5  27694  stirlinglem8  27697  stirlinglem11  27700  stirlinglem12  27701  stirlinglem13  27702  stirlinglem14  27703  stirlinglem15  27704  nfafv  27867  nfaov  27910  bnj1230  28880  bnj1476  28924  bnj900  29006  bnj958  29017  bnj1000  29018  bnj1014  29037  bnj1123  29061  bnj1307  29098  bnj1321  29102  bnj1384  29107  bnj1398  29109  bnj1408  29111  bnj1444  29118  bnj1445  29119  bnj1446  29120  bnj1447  29121  bnj1448  29122  bnj1449  29123  bnj1466  29128  bnj1467  29129  bnj1518  29139  bnj1519  29140  bnj1520  29141  bnj1525  29144  bnj1523  29146  cdleme26ee  30842  cdlemefs32sn1aw  30896  cdleme43fsv1snlem  30902  cdleme41sn3a  30915  cdleme32d  30926  cdleme32f  30928  cdleme40m  30949  cdleme40n  30950  ltrniotaval  31063  cdlemksv2  31329  cdlemkuv2  31349  cdlemk36  31395  cdlemk38  31397  cdlemkid  31418  cdlemk19x  31425  cdlemk11t  31428
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-cleq 2397  df-clel 2400  df-nfc 2529
  Copyright terms: Public domain W3C validator