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

Theorem nfcxfr 2429
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 2428 . 2  |-  ( F/_ x A  <->  F/_ x B )
41, 3mpbir 200 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    = wceq 1632   F/_wnfc 2419
This theorem is referenced by:  nfrab1  2733  nfrab  2734  nfdif  3310  nfun  3344  nfin  3388  nfpw  3649  nfpr  3693  nfsn  3704  nfop  3828  nfuni  3849  nfint  3888  nfiun  3947  nfiin  3948  nfiu1  3949  nfii1  3950  nfopab  4100  nfopab1  4101  nfopab2  4102  nfmpt  4124  nfmpt1  4125  nfsuc  4479  nfxp  4731  nfco  4865  nfcnv  4876  nfdm  4936  nfrn  4937  nfres  4973  nfima  5036  nfiota1  5237  nffv  5548  fvmptss  5625  fvmptf  5632  ralrnmpt  5685  f1ompt  5698  f1mpt  5801  fliftfun  5827  nfoprab1  5913  nfoprab2  5914  nfoprab3  5915  nfoprab  5916  nfmpt21  5930  nfmpt22  5931  nfmpt2  5932  ovmpt2s  5987  ov2gf  5988  ov3  6000  nfof  6099  nfofr  6100  nftpos  6285  fvopab5  6305  opabiota  6309  nfriota1  6328  riotaprop  6344  riotasv2s  6367  nfrecs  6406  nfrdg  6443  rdgsucmptf  6457  rdgsucmptnf  6458  frsucmpt  6466  frsucmptn  6467  nfixp  6851  nfixp1  6852  xpcomco  6968  nfsup  7218  nfoi  7245  cnfcom3clem  7424  dfac8clem  7675  axdclem  8162  iunfo  8177  pwfseqlem2  8297  pwfseqlem4a  8299  pwfseqlem4  8300  reclem2pr  8688  nfseq  11072  nfwrd  11442  nfsum1  12179  nfsum  12180  ptbasfi  17292  mbfsup  19035  itg1climres  19085  itg2splitlem  19119  itg2split  19120  nfitg1  19144  nfitg  19145  lgseisenlem2  20605  cnlnadjlem5  22667  dya2iocrrnval  23597  cvmcov  23809  nfcprod1  24132  nfcprod  24133  nfsymdif  24437  nfaltop  24586  nfprod1  25413  nfprod  25414  prodeqfv  25421  ltrinvlem  25509  sdclem1  26556  refsum2cnlem1  27811  fmuldfeqlem1  27815  fmuldfeq  27816  itgsinexplem1  27851  stoweidlem14  27866  stoweidlem16  27868  stoweidlem18  27870  stoweidlem22  27874  stoweidlem26  27878  stoweidlem27  27879  stoweidlem31  27883  stoweidlem32  27884  stoweidlem34  27886  stoweidlem35  27887  stoweidlem40  27892  stoweidlem41  27893  stoweidlem42  27894  stoweidlem44  27896  stoweidlem45  27897  stoweidlem46  27898  stoweidlem47  27899  stoweidlem48  27900  stoweidlem50  27902  stoweidlem51  27903  stoweidlem52  27904  stoweidlem53  27905  stoweidlem54  27906  stoweidlem57  27909  stoweidlem59  27911  stoweidlem62  27914  wallispilem5  27921  stirlinglem4  27929  stirlinglem5  27930  stirlinglem8  27933  stirlinglem11  27936  stirlinglem12  27937  stirlinglem13  27938  stirlinglem14  27939  stirlinglem15  27940  nfafv  28104  nfaov  28147  bnj1230  29151  bnj1476  29195  bnj900  29277  bnj958  29288  bnj1000  29289  bnj1014  29308  bnj1123  29332  bnj1307  29369  bnj1321  29373  bnj1384  29378  bnj1398  29380  bnj1408  29382  bnj1444  29389  bnj1445  29390  bnj1446  29391  bnj1447  29392  bnj1448  29393  bnj1449  29394  bnj1466  29399  bnj1467  29400  bnj1518  29410  bnj1519  29411  bnj1520  29412  bnj1525  29415  bnj1523  29417  cdleme26ee  31171  cdlemefs32sn1aw  31225  cdleme43fsv1snlem  31231  cdleme41sn3a  31244  cdleme32d  31255  cdleme32f  31257  cdleme40m  31278  cdleme40n  31279  ltrniotaval  31392  cdlemksv2  31658  cdlemkuv2  31678  cdlemk36  31724  cdlemk38  31726  cdlemkid  31747  cdlemk19x  31754  cdlemk11t  31757
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-cleq 2289  df-clel 2292  df-nfc 2421
  Copyright terms: Public domain W3C validator