Theorem nfbr 5147

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 5146	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴𝑅𝐵)
8	7	mptru 1549	1 ⊢ Ⅎ𝑥 𝐴𝑅𝐵

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785  Ⅎwnfc 2884   class class class wbr 5100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  sbcbr123  5154  nfpo  5548  nfso  5549  pofun  5560  nffr  5607  nfse  5608  nfco  5824  nfcnv  5837  dfdmf  5855  dfrnf  5909  nfdm  5910  dfrel4  6159  dffun6f  6517  nffv  6854  funfv2f  6933  fvopab5  6985  f1ompt  7067  fmptco  7086  nfiso  7280  nfofr  7641  ofrfval2  7655  tposoprab  8216  xpcomco  9009  nfoi  9433  tskwe  9876  cardmin2  9925  uniimadomf  10469  cardmin  10488  inar1  10700  lble  12108  rlim2  15433  ello1mpt  15458  rlimcld2  15515  o1compt  15524  nfsum1  15627  nfsum  15628  fsum00  15735  fsumrlim  15748  o1fsum  15750  nfcprod1  15845  nfcprod  15846  sumeven  16328  sumodd  16329  invfuc  17915  dprd2d2  19992  2ndcdisj  23417  ovoliunlem3  25478  mbfpos  25625  mbfposb  25627  mbfsup  25638  mbfinf  25639  i1fposd  25681  itg2splitlem  25722  itg2split  25723  isibl2  25740  nfitg  25749  cbvitg  25750  itggt0  25818  dvlipcn  25972  dvfsumle  25999  dvfsumleOLD  26000  dvfsumabs  26002  dvfsumlem2  26006  dvfsumlem2OLD  26007  dvfsumlem4  26009  dvfsumrlim  26011  dvfsum2  26014  rlimcnp  26948  lgamgulmlem2  27013  lgamgulmlem6  27017  dchrisumlema  27472  dchrisumlem2  27474  dchrisumlem3  27475  nosupbnd1  27699  nosupbnd2  27701  noinfbnd1  27714  noinfbnd2  27716  chirred  32489  iundisjf  32682  fmptcof2  32753  fsumiunle  32927  esumfsup  34254  esum2d  34277  measvunilem  34396  measvunilem0  34397  bj-opabco  37470  phpreu  37884  poimirlem26  37926  poimirlem27  37927  poimirlem28  37928  itggt0cn  37970  ftc1anclem5  37977  cdleme26ee  40765  cdlemefs32sn1aw  40819  cdleme41sn3a  40838  cdleme32d  40849  cdleme32f  40851  cdlemk38  41320  cdlemk11t  41351  monotoddzz  43329  oddcomabszz  43330  nfrelp  45334  permaxrep  45391  evth2f  45404  evthf  45416  rfcnpre3  45422  rfcnpre4  45423  rfcnnnub  45425  ssfiunibd  45700  uzub  45818  supxrleubrnmptf  45838  infrpgernmpt  45852  monoordxr  45869  monoord2xr  45871  caucvgbf  45876  cvgcaule  45878  fsumlessf  45966  fmul01  45969  fmul01lt1lem1  45973  fmul01lt1  45975  climinff  46000  idlimc  46015  limcperiod  46017  fnlimabslt  46066  limsupref  46072  limsupbnd1f  46073  climbddf  46074  limsuppnfd  46089  climinf2  46094  limsuppnf  46098  limsupubuz  46100  climinf2mpt  46101  climinfmpt  46102  limsupmnf  46108  limsupre2  46112  limsupmnfuz  46114  limsupre3  46120  limsupre3uz  46123  limsupreuz  46124  climuz  46131  limsupgt  46165  liminfreuz  46190  liminflt  46192  xlimpnfxnegmnf  46201  xlimmnf  46228  xlimpnf  46229  dfxlim2  46235  cncfshift  46261  cncficcgt0  46275  stoweidlem3  46390  stoweidlem26  46413  stoweidlem28  46415  stoweidlem31  46418  stoweidlem51  46438  stoweidlem52  46439  stoweidlem59  46446  stirling  46476  fourierdlem20  46514  fourierdlem79  46572  etransclem48  46669  sge0ltfirp  46787  sge0lempt  46797  meaiunincf  46870  iunhoiioolem  47062  pimltmnf2f  47084  pimgtpnf2f  47092  pimltpnf2f  47099  pimgtmnf2  47101  pimdecfgtioc  47102  issmff  47121  smfpimltxrmptf  47145  smfpreimagtf  47155  smflim  47164  smfpimgtxr  47167  smfpimgtxrmptf  47171  smfsup  47201  smfinflem  47204  smfinf  47205  nfafv2  47607  prmdvdsfmtnof1lem1  47973  dffun3f  50070  setrec2  50083