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

Theorem nfbr 4496
Description: Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
Hypotheses
Ref Expression
nfbr.1
nfbr.2
nfbr.3
Assertion
Ref Expression
nfbr

Proof of Theorem nfbr
StepHypRef Expression
1 nfbr.1 . . . 4
21a1i 11 . . 3
3 nfbr.2 . . . 4
43a1i 11 . . 3
5 nfbr.3 . . . 4
65a1i 11 . . 3
72, 4, 6nfbrd 4495 . 2
87trud 1404 1
Colors of variables: wff setvar class
Syntax hints:   wtru 1396  F/wnf 1616  F/_wnfc 2605   class class class wbr 4452
This theorem is referenced by:  sbcbr123  4503  sbcbrgOLD  4504  nfpo  4810  nfso  4811  pofun  4821  nffr  4858  nfse  4859  nfco  5173  nfcnv  5186  dfdmf  5201  dfrnf  5246  nfdm  5249  dffun6f  5607  nffv  5878  funfv2f  5942  fvopab5  5979  f1ompt  6053  fmptco  6064  nfiso  6220  ofrfval2  6557  tposoprab  7010  xpcomco  7627  nfoi  7960  tskwe  8352  cardmin2  8400  uniimadomf  8941  cardmin  8960  inar1  9174  lble  10520  rlim2  13319  ello1mpt  13344  rlimcld2  13401  o1compt  13410  nfsum1  13512  nfsum  13513  fsum00  13612  fsumrlim  13625  o1fsum  13627  nfcprod1  13717  nfcprod  13718  invfuc  15343  dprd2d2  17093  2ndcdisj  19957  ovoliunlem3  21915  mbfpos  22058  mbfposb  22060  mbfsup  22071  mbfinf  22072  i1fposd  22114  itg2splitlem  22155  itg2split  22156  isibl2  22173  nfitg  22181  cbvitg  22182  itggt0  22248  dvlipcn  22395  dvfsumle  22422  dvfsumabs  22424  dvfsumlem2  22428  dvfsumlem4  22430  dvfsumrlim  22432  dvfsum2  22435  rlimcnp  23295  dchrisumlema  23673  dchrisumlem2  23675  dchrisumlem3  23676  chirred  27314  iundisjf  27448  dfrel4  27454  fmptcof2  27502  esumfsup  28076  measvunilem  28183  measvunilem0  28184  lgamgulmlem2  28572  lgamgulmlem6  28576  itggt0cn  30087  ftc1anclem5  30094  monotoddzz  30879  oddcomabszz  30880  evth2f  31390  evthf  31402  rfcnpre3  31408  rfcnpre4  31409  rfcnnnub  31411  ssfiunibd  31509  fmul01  31574  fmul01lt1lem1  31578  fmul01lt1  31580  climinff  31617  idlimc  31632  limcperiod  31634  cncfshift  31676  cncficcgt0  31691  stoweidlem3  31785  stoweidlem26  31808  stoweidlem28  31810  stoweidlem31  31813  stoweidlem51  31833  stoweidlem52  31834  stoweidlem59  31841  stirling  31871  fourierdlem20  31909  fourierdlem79  31968  etransclem48  32065  cdleme26ee  36086  cdlemefs32sn1aw  36140  cdleme41sn3a  36159  cdleme32d  36170  cdleme32f  36172  cdlemk38  36641  cdlemk11t  36672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453
  Copyright terms: Public domain W3C validator