Theorem nfbr 5160

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

Step	Hyp	Ref	Expression
1		nfbr.1	. . . 4 ⊢ Ⅎ𝑥𝐴
2	1	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
3		nfbr.2	. . . 4 ⊢ Ⅎ𝑥𝑅
4	3	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝑅)
5		nfbr.3	. . . 4 ⊢ Ⅎ𝑥𝐵
6	5	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐵)
7	2, 4, 6	nfbrd 5159	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴𝑅𝐵)
8	7	mptru 1574	1 ⊢ Ⅎ𝑥 𝐴𝑅𝐵

Syntax hints:  ⊤wtru 1568  Ⅎwnf 1810  Ⅎwnfc 2916   class class class wbr 5111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112

This theorem is referenced by:  sbcbr123  5167  nfpo  5576  nfso  5577  pofun  5588  nffr  5635  nfse  5636  nfco  5852  nfcnv  5865  dfdmf  5887  dfrnf  5941  nfdm  5942  dfrel4  6190  dffun6f  6552  nffv  6892  funfv2f  6971  fvopab5  7024  f1ompt  7107  fmptco  7126  nfiso  7321  nfofr  7682  ofrfval2  7696  tposoprab  8258  xpcomco  9055  nfoi  9476  tskwe  9936  cardmin2  9985  uniimadomf  10529  cardmin  10548  inar1  10760  lble  12167  rlim2  15547  ello1mpt  15572  rlimcld2  15629  o1compt  15638  nfsum1  15741  nfsum  15742  fsum00  15850  fsumrlim  15863  o1fsum  15865  nfcprod1  15962  nfcprod  15963  sumeven  16445  sumodd  16446  invfuc  18034  dprd2d2  20116  2ndcdisj  23582  ovoliunlem3  25632  mbfpos  25779  mbfposb  25781  mbfsup  25792  mbfinf  25793  i1fposd  25835  itg2splitlem  25876  itg2split  25877  isibl2  25894  nfitg  25903  cbvitg  25904  itggt0  25972  dvlipcn  26122  dvfsumle  26149  dvfsumabs  26151  dvfsumlem2  26155  dvfsumlem4  26157  dvfsumrlim  26159  dvfsum2  26162  rlimcnp  27096  lgamgulmlem2  27160  lgamgulmlem6  27164  dchrisumlema  27618  dchrisumlem2  27620  dchrisumlem3  27621  nosupbnd1  27844  nosupbnd2  27846  noinfbnd1  27859  noinfbnd2  27861  chirred  32688  iundisjf  32875  fmptcof2  32943  fsumiunle  33114  esumfsup  34405  esum2d  34428  measvunilem  34547  measvunilem0  34548  bj-opabco  37755  phpreu  38178  poimirlem26  38220  poimirlem27  38221  poimirlem28  38222  itggt0cn  38264  ftc1anclem5  38271  cdleme26ee  41059  cdlemefs32sn1aw  41113  cdleme41sn3a  41132  cdleme32d  41143  cdleme32f  41145  cdlemk38  41614  cdlemk11t  41645  monotoddzz  43597  oddcomabszz  43598  nfrelp  45585  permaxrep  45642  evth2f  45662  evthf  45674  rfcnpre3  45680  rfcnpre4  45681  rfcnnnub  45683  ssfiunibd  45955  uzub  46072  supxrleubrnmptf  46092  infrpgernmpt  46106  monoordxr  46123  monoord2xr  46125  caucvgbf  46130  cvgcaule  46132  fsumlessf  46220  fmul01  46223  fmul01lt1lem1  46227  fmul01lt1  46229  climinff  46254  idlimc  46269  limcperiod  46271  fnlimabslt  46320  limsupref  46326  limsupbnd1f  46327  climbddf  46328  limsuppnfd  46343  climinf2  46348  limsuppnf  46352  limsupubuz  46354  climinf2mpt  46355  climinfmpt  46356  limsupmnf  46362  limsupre2  46366  limsupmnfuz  46368  limsupre3  46374  limsupre3uz  46377  limsupreuz  46378  climuz  46385  limsupgt  46419  liminfreuz  46444  liminflt  46446  xlimpnfxnegmnf  46455  xlimmnf  46482  xlimpnf  46483  dfxlim2  46489  cncfshift  46515  cncficcgt0  46529  stoweidlem3  46644  stoweidlem26  46667  stoweidlem28  46669  stoweidlem31  46672  stoweidlem51  46692  stoweidlem52  46693  stoweidlem59  46700  stirling  46730  fourierdlem20  46768  fourierdlem79  46826  etransclem48  46923  sge0ltfirp  47041  sge0lempt  47051  meaiunincf  47124  iunhoiioolem  47316  pimltmnf2f  47338  pimgtpnf2f  47346  pimltpnf2f  47353  pimgtmnf2  47355  pimdecfgtioc  47356  issmff  47375  smfpimltxrmptf  47399  smfpreimagtf  47409  smflim  47418  smfpimgtxr  47421  smfpimgtxrmptf  47425  smfsup  47455  smfinflem  47458  smfinf  47459  nfafv2  47879  prmdvdsfmtnof1lem1  48260  dffun3f  50380  setrec2  50393