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

Theorem nfcxfr 2416
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 2415 . 2  |-  ( F/_ x A  <->  F/_ x B )
41, 3mpbir 200 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    = wceq 1623   F/_wnfc 2406
This theorem is referenced by:  nfrab1  2720  nfrab  2721  nfdif  3297  nfun  3331  nfin  3375  nfpw  3636  nfpr  3680  nfsn  3691  nfop  3812  nfuni  3833  nfint  3872  nfiun  3931  nfiin  3932  nfiu1  3933  nfii1  3934  nfopab  4084  nfopab1  4085  nfopab2  4086  nfmpt  4108  nfmpt1  4109  nfsuc  4463  nfxp  4715  nfco  4849  nfcnv  4860  nfdm  4920  nfrn  4921  nfres  4957  nfima  5020  nfiota1  5221  nffv  5532  fvmptss  5609  fvmptf  5616  ralrnmpt  5669  f1ompt  5682  f1mpt  5785  fliftfun  5811  nfoprab1  5897  nfoprab2  5898  nfoprab3  5899  nfoprab  5900  nfmpt21  5914  nfmpt22  5915  nfmpt2  5916  ovmpt2s  5971  ov2gf  5972  ov3  5984  nfof  6083  nfofr  6084  nftpos  6269  fvopab5  6289  opabiota  6293  nfriota1  6312  riotaprop  6328  riotasv2s  6351  nfrecs  6390  nfrdg  6427  rdgsucmptf  6441  rdgsucmptnf  6442  frsucmpt  6450  frsucmptn  6451  nfixp  6835  nfixp1  6836  xpcomco  6952  nfsup  7202  nfoi  7229  cnfcom3clem  7408  dfac8clem  7659  axdclem  8146  iunfo  8161  pwfseqlem2  8281  pwfseqlem4a  8283  pwfseqlem4  8284  reclem2pr  8672  nfseq  11056  nfwrd  11426  nfsum1  12163  nfsum  12164  ptbasfi  17276  mbfsup  19019  itg1climres  19069  itg2splitlem  19103  itg2split  19104  nfitg1  19128  nfitg  19129  lgseisenlem2  20589  cnlnadjlem5  22651  dya2iocrrnval  23582  cvmcov  23794  nfsymdif  24366  nfaltop  24514  nfprod1  25310  nfprod  25311  prodeqfv  25318  ltrinvlem  25406  sdclem1  26453  refsum2cnlem1  27708  fmuldfeqlem1  27712  fmuldfeq  27713  itgsinexplem1  27748  stoweidlem14  27763  stoweidlem16  27765  stoweidlem18  27767  stoweidlem22  27771  stoweidlem26  27775  stoweidlem27  27776  stoweidlem31  27780  stoweidlem32  27781  stoweidlem34  27783  stoweidlem35  27784  stoweidlem40  27789  stoweidlem41  27790  stoweidlem42  27791  stoweidlem44  27793  stoweidlem45  27794  stoweidlem46  27795  stoweidlem47  27796  stoweidlem48  27797  stoweidlem50  27799  stoweidlem51  27800  stoweidlem52  27801  stoweidlem53  27802  stoweidlem54  27803  stoweidlem57  27806  stoweidlem59  27808  stoweidlem62  27811  wallispilem5  27818  stirlinglem4  27826  stirlinglem5  27827  stirlinglem8  27830  stirlinglem11  27833  stirlinglem12  27834  stirlinglem13  27835  stirlinglem14  27836  stirlinglem15  27837  nfafv  27999  nfaov  28039  bnj1230  28835  bnj1476  28879  bnj900  28961  bnj958  28972  bnj1000  28973  bnj1014  28992  bnj1123  29016  bnj1307  29053  bnj1321  29057  bnj1384  29062  bnj1398  29064  bnj1408  29066  bnj1444  29073  bnj1445  29074  bnj1446  29075  bnj1447  29076  bnj1448  29077  bnj1449  29078  bnj1466  29083  bnj1467  29084  bnj1518  29094  bnj1519  29095  bnj1520  29096  bnj1525  29099  bnj1523  29101  cdleme26ee  30549  cdlemefs32sn1aw  30603  cdleme43fsv1snlem  30609  cdleme41sn3a  30622  cdleme32d  30633  cdleme32f  30635  cdleme40m  30656  cdleme40n  30657  ltrniotaval  30770  cdlemksv2  31036  cdlemkuv2  31056  cdlemk36  31102  cdlemk38  31104  cdlemkid  31125  cdlemk19x  31132  cdlemk11t  31135
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-cleq 2276  df-clel 2279  df-nfc 2408
  Copyright terms: Public domain W3C validator