Theorem nfbr 5157

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

This proof depends on syntax axioms:  ⊤wtru 1570  Ⅎwnf 1812  Ⅎwnfc 2909   class class class wbr 5108

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109

This theorem is used by:  sbcbr123  5164  nfpo  5574  nfso  5575  pofun  5586  nffr  5633  nfse  5634  nfco  5850  nfcnv  5863  dfdmf  5885  dfrnf  5939  nfdm  5940  dfrel4  6188  dffun6f  6551  nffv  6891  funfv2f  6970  fvopab5  7023  f1ompt  7106  fmptco  7125  nfiso  7320  nfofr  7683  ofrfval2  7697  tposoprab  8256  xpcomco  9053  nfoi  9474  tskwe  9943  cardmin2  9992  uniimadomf  10535  cardmin  10554  inar1  10766  lble  12173  rlim2  15554  ello1mpt  15579  rlimcld2  15636  o1compt  15645  nfsum1  15748  nfsum  15749  fsum00  15857  fsumrlim  15870  o1fsum  15872  nfcprod1  15969  nfcprod  15970  sumeven  16451  sumodd  16452  invfuc  18040  dprd2d2  20122  2ndcdisj  23624  ovoliunlem3  25674  mbfpos  25821  mbfposb  25823  mbfsup  25834  mbfinf  25835  i1fposd  25877  itg2splitlem  25918  itg2split  25919  isibl2  25936  nfitg  25945  cbvitg  25946  itggt0  26014  dvlipcn  26164  dvfsumle  26191  dvfsumabs  26193  dvfsumlem2  26197  dvfsumlem4  26199  dvfsumrlim  26201  dvfsum2  26204  rlimcnp  27141  lgamgulmlem2  27205  lgamgulmlem6  27209  dchrisumlema  27663  dchrisumlem2  27665  dchrisumlem3  27666  nosupbnd1  27889  nosupbnd2  27891  noinfbnd1  27904  noinfbnd2  27906  chirred  32758  iundisjf  32945  fmptcof2  33013  fsumiunle  33184  esumfsup  34469  esum2d  34492  measvunilem  34611  measvunilem0  34612  bj-opabco  37860  phpreu  38283  poimirlem26  38325  poimirlem27  38326  poimirlem28  38327  itggt0cn  38369  ftc1anclem5  38376  cdleme26ee  41162  cdlemefs32sn1aw  41216  cdleme41sn3a  41235  cdleme32d  41246  cdleme32f  41248  cdlemk38  41717  cdlemk11t  41748  monotoddzz  43698  oddcomabszz  43699  nfrelp  45686  permaxrep  45743  evth2f  45763  evthf  45775  rfcnpre3  45781  rfcnpre4  45782  rfcnnnub  45784  ssfiunibd  46056  uzub  46173  supxrleubrnmptf  46193  infrpgernmpt  46207  monoordxr  46224  monoord2xr  46226  caucvgbf  46231  cvgcaule  46233  fsumlessf  46321  fmul01  46324  fmul01lt1lem1  46328  fmul01lt1  46330  climinff  46355  idlimc  46370  limcperiod  46372  fnlimabslt  46421  limsupref  46427  limsupbnd1f  46428  climbddf  46429  limsuppnfd  46444  climinf2  46449  limsuppnf  46453  limsupubuz  46455  climinf2mpt  46456  climinfmpt  46457  limsupmnf  46463  limsupre2  46467  limsupmnfuz  46469  limsupre3  46475  limsupre3uz  46478  limsupreuz  46479  climuz  46486  limsupgt  46520  liminfreuz  46545  liminflt  46547  xlimpnfxnegmnf  46556  xlimmnf  46583  xlimpnf  46584  dfxlim2  46590  cncfshift  46616  cncficcgt0  46630  stoweidlem3  46745  stoweidlem26  46768  stoweidlem28  46770  stoweidlem31  46773  stoweidlem51  46793  stoweidlem52  46794  stoweidlem59  46801  stirling  46831  fourierdlem20  46869  fourierdlem79  46927  etransclem48  47024  sge0ltfirp  47142  sge0lempt  47152  meaiunincf  47225  iunhoiioolem  47417  pimltmnf2f  47439  pimgtpnf2f  47447  pimltpnf2f  47454  pimgtmnf2  47456  pimdecfgtioc  47457  issmff  47476  smfpimltxrmptf  47500  smfpreimagtf  47510  smflim  47519  smfpimgtxr  47522  smfpimgtxrmptf  47526  smfsup  47556  smfinflem  47559  smfinf  47560  nfafv2  47983  prmdvdsfmtnof1lem1  48364  dffun3f  50488  setrec2  50501